摘要

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

全文