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

Abstract: Non-functional properties of the embedded software system arc 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 I=CBESD( Tool for Component-Based Embedded Software Designs) was extended with analysis and verification capabilities considering both of resource utilization and energy consumption propertics,which include the input/output mechanisms for resource interface automata and energy automata respectively, the pr}translation from a UML sectuence 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 component based system design analysis.

Key words: Embedded software design, Non-functional property verification, Component based design, Software verification tool.Interface automata