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

作     者：徐丙凤 胡军 曹东 黄志球 郭丽娟 张剑 XU Bing-feng;HU Jun;CAO Dong;HUANG Zhi-qiu;GUO Li-juan;ZHANG Jian

作者机构：南京航空航天大学信息科学与技术学院江苏南京210016 计算机软件新技术国家重点实验室(南京大学)江苏南京210093 南京航空航天大学自动化学院江苏南京210016 

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

出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)

年 卷 期：2010年第31卷第11期

页      码：2129-2137页

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

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

馆 藏 号：203173169...