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

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 concerned 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) has been extended with analysis and verification capabilities considering both of resource 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 component-based system design analysis.