构件化嵌入式软件设计模型验证工具的研究

基于模型设计与分析技术能够明显提高现代复杂嵌入式软件系统的可靠性，本文基于接口自动机模型设计实现了一个构件化嵌入式软件验证工具并进行了形式化验证。该工具的系统规约采用UML顺序图模型实现，能够对系统设计模型与场景式规约之间多种行为的一致性进行检验，并对实时接口自动机网络与具有时间约束顺序图模型的一致性行为进行检验。