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

《基于模型检查的嵌入式软件构件化分析与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、基于模型检查的嵌入式软件构件化分析与验证　　摘要：对嵌入式软件构件化进行准确分析与验证，能够为嵌入式系统安全、稳定的运行提供保障。提出一种基于模型检查的嵌入式软件构件化分析与验证方法。设计一种用于检查软件构件的模型，为嵌入式软件构件化分析与验证提供理论基础；将嵌入式软件系统模型用SMV语言的形式表达，利用SMV模型检查工具实现对嵌入式软件运行状态的分析与检验。实验结果表明，该模型能够对嵌入式软件构件化的非功能性方面的设计要求进行准确分析与验证，为嵌入式系统安全稳定的运行提供了保障。　　关键词：模型检查

2、；嵌入式软件；构件化；SMV　　中图分类号：TN911?34；TP391文献标识码：A文章编号：1004?373X（2016）24?0063?03　　Embeddedsoftwarecomponentanalysisandverificationbasedonmodelchecking　　NIEJienan　　（InstituteofHumanityInformationManagement，ChengduMedicalCollege，Chengdu610500，China）　　Abstract：Th

3、eembeddedsoftwarecomponentisanalyzedandvalidatedaccurately，whichmayprovidethesafeandstableoperationfortheembeddedsystem.Aanalysisandvalidationmethodoftheembeddedsoftwarecomponentbasedonmodelcheckingisput10forward.Akindofmodelusedtoexaminethesoftwarecomp

4、onentisdesigned，whichprovidesatheoreticalfoundationforanalysisandverificationoftheembeddedsoftwarecomponent.TheembeddedsoftwaresystemmodelisexpressedintheformofSMVlanguage.TheSMVmodelcheckingtoolisusedtoimplementanalysisandtestoftheembeddedsoftwarerunni

5、ngstatus.Theexperimentalresultsshowthatthemodelcanaccuratelyanalyzeandvalidatethenon?functionaldesignrequirementsoftheembeddedsoftwarecomponent，andprovidedthesafeguardfortheembeddedsystemsafeandstableoperation.　　Keywords：modelchecking；embeddedsoftware；c

6、omponent；SMV　　嵌入式系统各种功能的实现都离不开软件[1]，软件具有极其重要的意义[2]，它是影响嵌入式系统稳定运行的关键因素，一旦关键部位中嵌入式系统的软件失效[3]，轻则造成财产损失，重则使生命受到威胁[4]。与PC机中的软件相比，嵌入式系统中的软件既要满足其功能性设计要求[5]，又要满足其非功能性的设计要求，如软件的驱动程度、运算资源的占用程度、对能量的消耗程度等[6]。因此如何对嵌入式系统中的非功能性设计要求进行分析与验证，已经成为当前IT领域中的一个热点研究课题，受到专家学者的广

7、泛关注[7]。10　　目前，主要的嵌入式系统软件验证方法包括基于马尔科夫的验证方法[8]、基于定理证明的验证方法和基于调试代理软件的验证方法[9]。最常用的是基于马尔科夫的嵌入式软件验证方法。但利用传统方法进行嵌入式系统软件的验证，验证的项目主要为软件的功能性设计要求，并且只能在软件设计的后期才能进行验证，难以对非功能性的设计要求进行准确分析与验证，导致嵌入式软件的稳定性与安全性难以得到保障[10]。　　针对传统方法存在的缺陷，提出一种基于模型检查的嵌入式软件构件化分析与验证方法。利用SMV检查工具对

8、嵌入式软件运行状态进行分析与检验，实现对嵌入式软件的分析与验证。仿真实验证明了改进算法在嵌入式软件构件化分析与验证方面的优势。　　1嵌入式软件构件化验证模型设计　　对嵌入式系统中的软件进行构件化验证，主要通过重复使用模块化软件来建立嵌入式软件构件化验证的模型，实现对嵌入式系统软件的验证。　　通常情况下，一个完整的嵌入式系统软件包括多个子系统软件，其软件系统具有较高的构件化特征。对嵌入式系统中构件化软件进行分析与验证，能够为嵌入式系统安全稳定的运行提供保障