GMC: A Performance Model Checker for Concurrent Systems
In consideration of public security and common wealth, functional correctness and immediacy measures of concurrent systems must be verified. Compared to functional verification, performance evaluation aims at obtaining quantitative measures of the system to test whether reliability-related properties are promised in all conditions. In this paper, concurrent systems are formalized and expressed in the form of IMC, a mixed model for describing both action or state based systems, and properties of these systems are converted into aCSL formulae. Equipped with an improved numerical algorithm and graphics user interface, the model checker GMC can be used for handling a variety of performance evaluation problems. The paper also analyzes the data structure and architecture of GMC in detail. The efficiency of GMC is discussed and some future improving methods are also given in this paper.
performance evaluation interactive markov chains concurrent systems model checking
Jianfeng Chen Jinzhao Wu
Chengdu Institute of Computer ApplicationsChinese Academy of SciencesChengdu, China Beijing Jiaotong University, Beijing, China Guangxi University For Nationalities, Nanning, China
国际会议
成都
英文
1-5
2010-08-20（万方平台首次上网日期，不代表论文的发表时间）