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

Embedded software component analysis and verification based on model checking

作　　者：聂捷楠[1] 

机构地区：[1]成都医学院人文信息管理学院,四川成都610500

出　　处：《现代电子技术》2016年第24期63-65,70,共4页Modern Electronics Technique

基　　金：四川省教育厅项目(14ZB0241)

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

关 键 词：模型检查 嵌入式软件 构件化 SMV 

分 类 号：TN911-34[电子电信—通信与信息系统] TP391[电子电信—信息与通信工程]