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

中国科技论文在线 构件化嵌入式软件设计模型非功能性质 验证的工具实现1 1 1 2 1 1 1 徐丙凤 , 胡军 , 曹东 , 黄志球 , 郭丽娟 , 张剑 1 南京航空航天大学 信息科学与技术学院，南京(210016) 2 南京航空航天大学 自动化学院，南京(210016) 摘 要：嵌入式软件的非功能性质是系统高可靠性的重要构成部分。传统的嵌入式软件可靠 性保障技术主要关注于系统开发后期，缺乏有效工具对系统设计的非功能性质进行分析与验 证。本文对基于接口自动机模型的构件化嵌入式软件设计验证原型工具 T-CBESD(Tool for Component-Based Embedded Software Designs)进行了资源及能耗等非功能性质验证功能的 扩展设计与实现。包括：资源接口自动机和能耗接口自动机模型的输入输出接口设计、UML 顺序图模型的预处理、带非功能语义信息的组合系统状态空间数据结构的设计、非实时资源 使用性质与实时相关能量消耗特征验证算法的实现，以及一个通信构件组合系统的实例应用 分析。 关键词：嵌入式软件设计；非功能性质验证；构件化设计；软件验证工具；接口自动机 1 引言 嵌入式计算系统已经广泛的应用于生活中的各个领域，如：交通、能源、医疗、控制、 通信、军事等。近年来随着计算机硬件性能的不断提高，嵌入式系统中软件的规模和复杂性 不断增加，使软件对整个系统的影响逐渐占据了统治地位。关键系统中的嵌入式软件失效将 会导致生命与财产的重大损失。与一般软件系统主要只考虑功能特征相比, 嵌入式软件必须 同时要满足其在非功能方面的性质要求(如: 实时性、系统资源的可使用性、 能量消耗特征 等) 。复杂嵌入式软件中各类非功能属性的分析与验证已成为当前嵌入式计算领域的一个研 究热点[1,2,3,4] 。目前工业界常用的嵌入式软件测试和调试方法(如：在处理器中嵌入ICE 功能， 调试代理软件，JTAG 模拟等)主要用于检查系统功能性质；同时，从软件工程角度来看，这 些方法都是在系统的开发中后期阶段所使用，而在嵌入式软件设计与分析的前期阶段还缺乏 有效的方法和工具对系统设计的非功能性质进行分析与验证。 本文基于接口自动机模型对构件化嵌入式软件设计(CBESD: Component-Based Embedded Software Designs) 的分析与验证方法展开进一步研究，对一个原型工具T-CBESD(a Tool for CBESD)[5]进行了系统资源和能耗等非功能性质验证方面的扩展。T-CBESD 是我们 设计的一个基于Eclipse 开放平台的构件化嵌入式软件设计分析与验证工具，在相关工作[5] 中已完成了基于场景式规约的系统非实时以及实时行为分析与验证功能部分的实现。本文工 作则主要进一步完成了对系统非实时资源使用性质以及与时间相关的能耗性质这两方面的 分析与验证功能实现；使得T-CBESD 的验证框架更为完整。工具最终目的是可以应用于构 件化嵌入式软件开发的设计建模阶段；不仅可以对设计者所关心的关键功能性质进行验证， 同时也可以对重要的系统资源以及与能耗相关的非功能性质进行严格形式化分析和验证，从 而提高系统可靠性的可信度。 本文内容安排如下：第2 节给出了针对系统设计的资源以及能耗验证的理论基础，包括： 描述系统动态行为的资源以及能耗接口自动机模型，基于场景的系统规约描述模型，以及形 1 本课题得到高等学校博士学科点专项科研基金资助课题(20070287052)的资助。 -1- 中国科技论文在线 式化分析与验证算法等。第3 节中给出了对T-CBESD 扩展非功能性质验证模块的基本设计 与实现思想，包括：资源及能耗接口自动机模型的输入输出接口设计、