System resource utilization analysis based on model checking method

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

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)219-226
Number of pages8
JournalInformatica (Ljubljana)
Volume29
Issue number2
Publication statusPublished - 2005 Jun 1

Fingerprint

Model checking
Model Checking
Resources
Temporal logic
Formal methods
Formal Methods
Performance Model
Temporal Logic
Counterexample
System Performance
Model

Keywords

  • LTL
  • Model Checking
  • Myrinet NIC
  • Property Specification
  • SPIN
  • Temporal Logic

ASJC Scopus subject areas

  • Software

Cite this

System resource utilization analysis based on model checking method. / Bang, Ki Seok; Jin, Hyun Wook; Chuck-Yoo, ; Choi, Jin Young.

In: Informatica (Ljubljana), Vol. 29, No. 2, 01.06.2005, p. 219-226.

Research output: Contribution to journalArticle

Bang, KS, Jin, HW, Chuck-Yoo, & Choi, JY 2005, 'System resource utilization analysis based on model checking method', Informatica (Ljubljana), vol. 29, no. 2, pp. 219-226.
Bang, Ki Seok ; Jin, Hyun Wook ; Chuck-Yoo, ; Choi, Jin Young. / System resource utilization analysis based on model checking method. In: Informatica (Ljubljana). 2005 ; Vol. 29, No. 2. pp. 219-226.
@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 = "6",
day = "1",
language = "English",
volume = "29",
pages = "219--226",
journal = "Informatica",
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/1

Y1 - 2005/6/1

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

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

M3 - Article

AN - SCOPUS:24744467631

VL - 29

SP - 219

EP - 226

JO - Informatica

JF - Informatica

SN - 0350-5596

IS - 2

ER -