T-CBESD:一个构件化嵌入式软件设计模型验证工具

摘要：

现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期.本文在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Designs).工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景式规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题.工具设计与实现内容包括:输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现以及通信构件组合系统的实例应用分析.

关键词：嵌入式软件设计、构件化设计、软件验证、接口自动机、模型检验工具

所属期刊栏目：31

分类号：TP311(计算技术、计算机技术)

资助基金：航空基金项目2007ZD52043;教育士点基金项目20070287052

在线出版日期：2011-03-09（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：2129-2137