摘要
现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期.本文在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Designs).工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景式规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题.工具设计与实现内容包括:输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现以及通信构件组合系统的实例应用分析.
High reliability requirements of modern embedded software system need effective model-based techniques for system designs and analysis. Traditional methods in embedded computing domain mostly concerned the implementation and testing phrase. In this paper, a prototype T-CBESD （Tool for Component-Based Embedded Software Designs ） has been designed, which is based on the theory of interface automata and is implemented as a plug-in module on the open-source platform Eclipse. The tool accepts UML sequence diagrams as the input system specification directly, checking several different kinds of behavioral consistency problems between the system design models and scenario-based specifications. By using timing constraint inequality of message events, the tool can verify whether the behaviors in real-time interface networks satisfy the sequence diagrams with real-time limitations. The designs and implementations of this work include the input/output mechanisms, the pre-translation from sequence diagrams to a set of message event sequences,the state space data structure designs, detail implementation issues of several verification algorithms and a component-based system verification example.
出处
《小型微型计算机系统》
CSCD
北大核心
2010年第11期2129-2137,共9页
Journal of Chinese Computer Systems
基金
航空基金项目(2007ZD52043)资助
教育士点基金项目(20070287052)资助
关键词
嵌入式软件设计
构件化设计
软件验证
接口自动机
模型检验工具
embedded software design
component-based design
software verification
interface automata
model checking tool
