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

【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.更多还原