Title :
Abstraction framework and complexity of model checking based on the Promela models
Author :
Chen Daoxi ; Zhang Guangquan ; Fan Jianxi
Author_Institution :
Sch. of Comput. Sci. & Technol., Soochow Univ., Suzhou, China
Abstract :
Automated model checking shortcomings is prone to state explosion. In this paper, we propose abstraction framework based on Promela models, and transform the source of Promela models to the abstract target of Promela models. On this basis, we analyze the reasons for the complexity of model checking based on Promela models. Finally we reduce the number of state-generated under the condition of verification property unchanged in the ATM example. These show that the abstraction framework reduce the complexity of model checking.
Keywords :
computational complexity; formal verification; software reliability; Promela models; abstraction framework; automated model checking shortcomings; formal verification technique; software system reliability; verification property; Application software; Computer science; Educational technology; Embedded computing; Embedded software; Explosions; Hardware; Software systems; Space technology; State-space methods; Abstraction framework; Complexity of model checking; Promela models;
Conference_Titel :
Computer Science & Education, 2009. ICCSE '09. 4th International Conference on
Conference_Location :
Nanning
Print_ISBN :
978-1-4244-3520-3
Electronic_ISBN :
978-1-4244-3521-0
DOI :
10.1109/ICCSE.2009.5228206