System resource utilization analysis based on model checking method

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

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


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)
Issue number2
Publication statusPublished - 2005 Jun


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

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Computer Science Applications
  • Artificial Intelligence


Dive into the research topics of 'System resource utilization analysis based on model checking method'. Together they form a unique fingerprint.

Cite this