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

T-CBESD:a Formal Verification Tool for Component-based Embedded Software Designs

作　　者：徐丙凤[1] 胡军[1,2] 曹东[3] 黄志球[1] 郭丽娟[1] 张剑[1] 

机构地区：[1]南京航空航天大学信息科学与技术学院,江苏南京210016 [2]计算机软件新技术国家重点实验室(南京大学),江苏南京210093 [3]南京航空航天大学自动化学院,江苏南京210016

出　　处：《小型微型计算机系统》2010年第11期2129-2137,共9页Journal of Chinese Computer Systems

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

摘　　要：现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期.本文在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.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]