Modeling And Analyzing Trustworthy Embedded Softwares In Model Driven Architecture

Embedded systems and their applications emerge continuously with the rapid upgrading of hardware performance and rapid development of communications and networks. Software plays an important role in an embedded system. How to use modern software engineering methods and techniques, reduce the complexity of software development, meet the constantly evaluation of customer requirements, reduce development costs and improve software trustworthiness has become an important topic in the field of embedded software development.Separating the application description from the platform specific implementation is a promising solution to reduce software development time, meet contant evaluation of customer requirements and reduce development costs. MDA (Model Driven Architecture, MDA) is one of the most attractive approaches to achieving this goal at present. In the early design phase of MDA, alternative solutions to the target system can be investigated and compared. So software development risks can be minimized.Models are the most important objects during software development processes in MDA. UML has become the de facto standard modeling language for software development. And it is recommended by OMG to describe models in MDA. But UML lacks the ability to describe non-functional properties which are important in trustworthy software development processes. A new UML profile dedicated for modeling and analysis of real-time and embedded (MARTE) systems is recently presented by OMG to describe non-function properties in an embedded system. MARTE stereotypes and tags are annotated on the related nodes in a UML diagram in this thesis. A UML diagram annotated with MARTE is expressed as UML/MARTE.Formal methods are important means to improve software trustworthy. To formally describe embedded systems, timed colored Petri net with inhibitor arcs (TCPNIA) is proposed in thesis. Model checking and analysis methods for TCPNIA models are also proposed. In order to formally verify and analyze UML models using TCPNIA in the early development stage of MDA, model transformation methods from UML/MARTE to TCPNIA are proposed.Contributions of this thesis are summarized as follows.(1) Methods to annotate non-functional properties on UML diagrams with MARTE Profile are proposed. UML diagrams can be annotated hierarchically using the methods in this thesis through selecting appropriate nodes in activity diagrams and sequence diagrams. The hierarchical method can improve the reusability of models and related verification results. Formal definitions of elements in a UML/MARTE model are proposed. They provide foundation for formal model transformations and analyses.(2) TCPNIA model is proposed. It integrates characteristics of timed Petri nets, colored Petri nets and inhibitor arcs. Energy consuming and data process functions are introduced for each transition in the model. Formal syntax and semantics of the TCPNIA model are defined. It can not only model functional and non-functional propertis of a complex system, but also make full use of existing Petri nets analysis techniques. TCPNIA model provides a foundation for modeling and analyzing real-time embedded systems with Petri nets.(3) An algorithm for transforming a TCPNIA model into a timed automaton is proposed. A conflict mediation mechanism is introduced in the algorithm for maintaining the semantics of timed transitions in the corresponding timed automaton. The method also applies for verifing general timed Petri nets using Uppaal.(4) A task scheduling algorithm with time and resources constraints for TCPNIA is proposed. The algorithm has considered parallel executions for time consuming calculation in a path. In order to improve the reusability of models' analysis results and computing efficiency, decomposition and composition methods for schedulable paths are analyzed. Depth-first recursive search method is used. State explosion problem can be mitigated for only a part of the state spaces are generated.(5) Model transformation methods from UML/MARTE to TCPNIA are proposed in graphical and formal systax forms respectively. Pointcuts in aspects are determined by the characteristics of a UML model in these methods. Automatic aspect generating algorithms are proposed. Automatic composing algorithms for TCPNIA models are proposed based on aspect-oriented weaving rules. These methods provide theoretical foundation for developing a tool to transform a UML/MARTE model into a TCPNIA model.