构件化嵌入式软件设计模型非功能性质验证的工具实现

作者：徐丙凤; 胡军; 曹东; 黄志球; 郭丽娟; 张剑

来源：计算机科学, 2010, (08): 156-163.

• 嵌入式软件设计
• 非功能性质验证
• 构件化设计
• 软件验证工具
• 接口自动机 Embedded software design
• Non-functional property verification
• Component-based design
• Software verification tool
• Interface automata

嵌入式软件的非功能性质是系统高可靠性的重要构成部分。传统的嵌入式软件可靠性保障技术主要关注于系统开发后期,缺乏有效工具对系统设计的非功能性质进行分析与验证。对基于接口自动机模型的构件化嵌入式软件设计验证原型工具T-CBESD(Tool for Component-based Embedded Software Designs)进行了资源及能耗等非功能性质验证功能的扩展设计与实现,包括:资源接口自动机和能耗接口自动机模型的输入输出接口设计、UML顺序图模型的预处理、带非功能语义信息的组合系统状态空间数据结构的设计、非实时资源使用性质与实时相关能量消耗特征验证算法的实现,以及一个通信构件组合系统的...

• 单位
  自动化学院; 计算机软件新技术国家重点实验室; 南京大学; 南京航空航天大学