GMC: A performance model checker for concurrent systems
Jianfeng Chen, Jinzhao Wu · 2010
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.