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