文章基本信息

标题：System Resource Utilization Analysis Based on Model Checking Method
本地全文：下载
作者：K.-S. Bang ; H.-W. Jin ; C. Yoo 等
期刊名称：Informatica
印刷版ISSN：1514-8327
电子版ISSN：1854-3871
出版年度：2005
卷号：29
期号：2
出版社：The Slovene Society Informatika, Ljubljana
摘要：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.
关键词：Model Checking; Temporal Logic; Property Specification; SPIN; LTL; Myrinet NIC