System resource utilization analysis based on model checking method

Ki Seok Bang; Hyun Wook Jin; Chuck-Yoo; Jin Young Choi

System resource utilization analysis based on model checking method

Ki Seok Bang, Hyun Wook Jin, Chuck-Yoo, Jin Young Choi

School of Cybersecurity

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

Abstract

Model checking method is a widely used formal method for proving whether or not a given model satisfies properties, and for producing counter examples if the model does not satisfy properties. In this paper, we show model checking methods can be used for resource utilization analysis of systems. We specify system utilization properties using temporal logic called LTL, and find a bottleneck of system performance using model checking.

Original language	English
Pages (from-to)	219-226
Number of pages	8
Journal	Informatica (Ljubljana)
Volume	29
Issue number	2
Publication status	Published - 2005 Jun

Keywords

LTL
Model Checking
Myrinet NIC
Property Specification
SPIN
Temporal Logic

ASJC Scopus subject areas

Software
Theoretical Computer Science
Computer Science Applications
Artificial Intelligence

Cite this

@article{1ac164fa1b56484cb3dca6575999e083,

title = "System resource utilization analysis based on model checking method",

abstract = "Model checking method is a widely used formal method for proving whether or not a given model satisfies properties, and for producing counter examples if the model does not satisfy properties. In this paper, we show model checking methods can be used for resource utilization analysis of systems. We specify system utilization properties using temporal logic called LTL, and find a bottleneck of system performance using model checking.",

keywords = "LTL, Model Checking, Myrinet NIC, Property Specification, SPIN, Temporal Logic",

author = "Bang, {Ki Seok} and Jin, {Hyun Wook} and Chuck-Yoo and Choi, {Jin Young}",

year = "2005",

month = jun,

language = "English",

volume = "29",

pages = "219--226",

journal = "Informatica (Ljubljana)",

issn = "0350-5596",

publisher = "Slovene Society Informatika",

number = "2",

}

TY - JOUR

T1 - System resource utilization analysis based on model checking method

AU - Bang, Ki Seok

AU - Jin, Hyun Wook

AU - Chuck-Yoo,

AU - Choi, Jin Young

PY - 2005/6

Y1 - 2005/6

N2 - Model checking method is a widely used formal method for proving whether or not a given model satisfies properties, and for producing counter examples if the model does not satisfy properties. In this paper, we show model checking methods can be used for resource utilization analysis of systems. We specify system utilization properties using temporal logic called LTL, and find a bottleneck of system performance using model checking.

AB - Model checking method is a widely used formal method for proving whether or not a given model satisfies properties, and for producing counter examples if the model does not satisfy properties. In this paper, we show model checking methods can be used for resource utilization analysis of systems. We specify system utilization properties using temporal logic called LTL, and find a bottleneck of system performance using model checking.

KW - LTL

KW - Model Checking

KW - Myrinet NIC

KW - Property Specification

KW - SPIN

KW - Temporal Logic

UR - http://www.scopus.com/inward/record.url?scp=24744467631&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:24744467631

SN - 0350-5596

VL - 29

SP - 219

EP - 226

JO - Informatica (Ljubljana)

JF - Informatica (Ljubljana)

IS - 2

ER -

System resource utilization analysis based on model checking method

Abstract

Keywords

ASJC Scopus subject areas

Other files and links

Fingerprint

Cite this