基于模型检查的嵌入式软件构件化分析与验证.docVIP

基于模型检查的嵌入式软件构件化分析与验证 　　摘 要： 对嵌入式软件构件化进行准确分析与验证，能够为嵌入式系统安全、稳定的运行提供保障。提出一种基于模型检查的嵌入式软件构件化分析与验证方法。设计一种用于检查软件构件的模型，为嵌入式软件构件化分析与验证提供理论基础；将嵌入式软件系统模型用SMV语言的形式表达，利用SMV模型检查工具实现对嵌入式软件运行状态的分析与检验。实验结果表明，该模型能够对嵌入式软件构件化的非功能性方面的设计要求进行准确分析与验证，为嵌入式系统安全稳定的运行提供了保障。 　　关键词： 模型检查； 嵌入式软件； 构件化； SMV 　　中图分类号： TN911?34； TP391 文献标识码： A 文章编号： 1004?373X（2016）24?0063?03 　　Embedded software component analysis and verification based on model checking 　　NIE Jienan 　　（Institute of Humanity Information Management， Chengdu Medical College， Chengdu 610500， China） 　　Abstract： The embedded software component is analyzed and validated accurately， which may provide the safe and stable operation for the embedded system. A analysis and validation method of the embedded software component based on model checking is put forward. A kind of model used to examine the software component is designed， which provides a theoretical foundation for analysis and verification of the embedded software component. The embedded software system model is expressed in the form of SMV language. The SMV model checking tool is used to implement analysis and test of the embedded software running status. The experimental results show that the model can accurately analyze and validate the non?functional design requirements of the embedded software component， and provided the safeguard for the embedded system safe and stable operation. 　　Keywords： model checking； embedded software； component； SMV 　　嵌入式系统各种功能的实现都离不开软件[1]，软件具有极其重要的意义[2]，它是影响嵌入式系统稳定运行的关键因素，一旦关键部位中嵌入式系统的软件失效[3]，轻则造成财产损失，重则使生命受到威胁[4]。与PC机中的软件相比，嵌入式系统中的软件既要满足其功能性设计要求[5]，又要满足其非功能性的设计要求，如软件的驱动程度、运算资源的占用程度、对能量的消耗程度等[6]。因此如何对嵌入式系统中的非功能性设计要求进行分析与验证，已经成为当前IT领域中的一个热点研究课题，受到专家学者的广泛关注[7]。 　　目前，主要的嵌入式系统软件验证方法包括基于马尔科夫的验证方法[8]、基于定理证明的验证方法和基于调试代理软件的验证方法[9]。最常用的是基于马尔科夫的嵌入式软件验证方法。但利用传统方法进行嵌入式系统软件的验证，验证的项目主要为软件的功能性设计要求，并且只能在软件设计的后期才能进行验证，难以对非功能性的设计要求进行准确分析与验证，导致嵌入式软件的稳定性与安全性难以得到保障[10]。 　　针对传统方法存在的缺陷，提出一种基于模型检查的嵌入式软件构件化分析与验证方法。利用SMV检查工具对嵌入式软件运行状态进行分析与检验，实现对嵌入式软件的分析与验证。仿真实验证明了改进