DocumentCode :
3229861
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
fYear :
2009
fDate :
25-28 July 2009
Firstpage :
857
Lastpage :
861
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;
fLanguage :
English
Publisher :
ieee
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
Type :
conf
DOI :
10.1109/ICCSE.2009.5228206
Filename :
5228206
Link To Document :
بازگشت