所有作者：徐丙凤 胡军 曹东 黄志球 郭丽娟 张剑
作者单位：南京航空航天大学信息科学与技术学院
论文摘要：现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术。传统的嵌入式软件可靠性保障技术主要关注于系统开发后期。本文在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD (Tool for Component-Based Embedded Software Designs)。工具直接使用UML顺序图模型作为系统规约，可以检验系统设计模型与场景式规约之间多种行为一致性问题；并使用消息事件的时间约束不等式，检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题。工具设计与实现内容包括：输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现以及通信构件组合系统的实例应用分析。
关键词： 嵌入式软件设计 构件化设计 软件验证 接口自动机 模型检验工具
免费下载《T-CBESD: 一个构件化嵌入式软件设计模型验证工具》PDF全文（已停止下载）
本站“论文下载”文章收集整理于“中国科技论文在线”，由于各种原因，本站已暂停论文下载！请前往“中国科技论文在线http://www.paper.edu.cn/”免费下载！
指出，范文大全立刻进行改正或删除有关内容! 
当前位置：