Abstraction Framework and Complezity of Model Checking Based on the Promela Models

摘要：

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.

关键词： Promela models Abstraction framework Complezity of model checking

作者: CHEN Daoxi ZHANG Guangquan FAN Jianxi

作者单位: School of Computer Science and Technology Soochow University Suzhou, 215006, China Suzhou Senior Tec School of Computer Science and Technology Soochow University Suzhou, 215006, China State Key Lab.of School of Computer Science and Technology Soochow University Suzhou, 215006, China

会议类型: 国际会议

会议名称: 第四届国际计算机新科技与教育学术会议(2009 4th International Conference on Computer Science & Education)

会议地点: 南京

会议语种:英文

页码: 857-861

在线出版日期: 2009-07-25（万方平台首次上网日期，不代表论文的发表时间）