| T-CBESD:一个构件化嵌入式软件设计模型验证工具 |
| |
| 引用本文： | 徐丙凤,胡军,曹东,黄志球,郭丽娟,张剑.T-CBESD:一个构件化嵌入式软件设计模型验证工具[J].小型微型计算机系统,2010,31(11). |
| |
| 作者姓名： | 徐丙凤 胡军 曹东 黄志球 郭丽娟 张剑 |
| |
| 作者单位： | 南京航空航天大学信息科学与技术学院;计算机软件新技术国家重点实验室(南京大学);南京航空航天大学自动化学院; |
| |
| 基金项目： | 航空基金项目，教育士点基金项目 |
| |
| 摘 要： | 现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期.本文在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Designs).工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景式规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题.工具设计与实现内容包括:输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现以及通信构件组合系统的实例应用分析.
|
| 关 键 词： | 嵌入式软件设计 构件化设计 软件验证 接口自动机 模型检验工具 |
T-CBESD: a Formal Verification Tool for Component-based Embedded Software Designs |
| |
| XU Bing-feng,HU Jun,CAO Dong,HUANG Zhi-qiu,GUO Li-juan,ZHANG Jian.T-CBESD: a Formal Verification Tool for Component-based Embedded Software Designs[J].Mini-micro Systems,2010,31(11). |
| |
| Authors: | XU Bing-feng HU Jun CAO Dong HUANG Zhi-qiu GUO Li-juan ZHANG Jian |
| |
| Affiliation: | XU Bing-feng1,HU Jun1,3,CAO Dong2,HUANG Zhi-qiu1,GUO Li-juan1,ZHANG Jian11(College of Information Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)2(College of Automation Engineering,China)3(State Key Laboratory for Novel Software Technology Nanjing University,Nanjing 210093,China) |
| |
| Abstract: | 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 t... |
| |
| Keywords: | embedded software design component-based design software verification interface automata model checking tool |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
