Title :
GMC: A performance model checker for concurrent systems
Author :
Chen, Jianfeng ; Wu, Jinzhao
Author_Institution :
Chengdu Inst. of Comput. Applic., Chinese Acad. of Sci., Chengdu, China
Abstract :
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.
Keywords :
concurrent engineering; data structures; formal verification; graphical user interfaces; software architecture; software performance evaluation; CSL formula; GMC architecture; concurrent system; data structure; functional verification; graphics model checker; graphics user interface; performance model checker; public security; reliability related property; state based system; Computational modeling; Hardware; concurrent systems; interactive markov chains; model checking; performance evaluation;
Conference_Titel :
Advanced Computer Theory and Engineering (ICACTE), 2010 3rd International Conference on
Conference_Location :
Chengdu
Print_ISBN :
978-1-4244-6539-2
DOI :
10.1109/ICACTE.2010.5579829
