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

Tool Implementation of Non-functional Verification for Component-based Embedded Software Designs

作　　者：徐丙凤[1] 胡军[1,2] 曹东[3] 黄志球[1] 郭丽娟[1] 张剑[1] 

机构地区：[1]南京航空航天大学信息科学与技术学院,南京210016 [2]南京大学计算机软件新技术国家重点实验室,南京210093 [3]南京航空航天大学自动化学院,南京210016

出　　处：《计算机科学》2010年第8期156-163,共8页Computer Science

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

摘　　要：嵌入式软件的非功能性质是系统高可靠性的重要构成部分。传统的嵌入式软件可靠性保障技术主要关注于系统开发后期,缺乏有效工具对系统设计的非功能性质进行分析与验证。对基于接口自动机模型的构件化嵌入式软件设计验证原型工具T-CBESD(Tool for Component-based Embedded Software Designs)进行了资源及能耗等非功能性质验证功能的扩展设计与实现,包括:资源接口自动机和能耗接口自动机模型的输入输出接口设计、UML顺序图模型的预处理、带非功能语义信息的组合系统状态空间数据结构的设计、非实时资源使用性质与实时相关能量消耗特征验证算法的实现,以及一个通信构件组合系统的实例应用分析。Non-functional properties of the embedded software system are considered as one of the important features for the high reliability assurance of whole system. Traditional reliability methods in embedded computing domain mostly concern the functional implementation and testing phrase, without effective tools supporting the analysis and verification of the system designs, especially for the non-functional properties. In this paper, a prototype T-CBESD（Tool for Component-Based Embedded Software Designs） was extended with analysis and verification capabilities considering both of re source utilization and energy consumption properties, which include the input/output mechanisms for resource interface automata and energy automata respectively, the pre-translation from a UML sequence diagram to a set of message event sequences, the state space data structure designs with non-functional semantics, the implementation issues of several analysis and verification algorithms for resource and energy consumption properties, and an example of a componentbased system design analysis.

关 键 词：嵌入式软件设计 非功能性质验证 构件化设计 软件验证工具 接口自动机 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]