| In recent years, with the rapid improvement of more powerful hardware in embedded systems, the size and complexity of embedded software are increasing rapidly too, and the embedded software has been regarded as one of the most dominate factors influencing the functionality and quality of the whole system, ensuring the reliability of embedded software is becoming more and more difficult. As a result of the traditional embedded softeware design approaches can not meet the high reliability requirements of modern embedded software design, so embedded software design must be integrated with the approaches of software engineering, such as component-based design, model driven architecture, formal specification and verification, and etc. Nowadays, model-based approaches are becoming the hot research issues for designing embedded software.Formal methods are the theories, technologies and tools based on maths which are used for realizing restrict reasoning in the development of computing systems. As a result of high reliability requirements of embedded software system, it is effective to increase the software reliability by use of formal verification technology. Therefore, introducing formal method in specifying requirements, and generating software architecture models which keep formal semantics from formal specification can increase the reliability of embedded software design.In this thesis, how to transform requirements specification to SA models of embedded software is discussed. The main contributions of this thesis are as follows:(1) In order to solve the problem that the SA models, which are created from natural language specifications, are often inaccurate or ambiguous, a transformation framework from requirements specification to SA models of embedded software is proposed based on the current research of transforming natural language specifications to SA models, moreover, an MDE based transformation framework for transforming formal specifications to SA models is proposed. The SA models, which are generated by this transformation framework, keep formal semantics, and can increase the reliability of SA design for embedded software essentially.(2) In order to solve the problem that the transformation from temporal specifications to SA models of embedded software, an MDE based approach for transforming LOTOS specifications to UML-RT models is proposed. UML-RT is widely used in modeling the software architectures of real-time and embedded systems, but UML-RT models are often inaccurate or ambiguous, because they are created from natural language specifications. In order to obtain more accurate UML-RT models, UML-RT models need to be given formal semantics. LOTOS is a process algebra fit for describing and verifying temporal specifications of embedded software. Based on the transformation framework from requirements specification to SA models, LOTOS is used to describe the temporal specifications of embedded software, and the transformation from LOTOS specifications to UML-RT models is realized by establishing a mechanism for translating LOTOS into UML-RT. The instance shows this approach can increase the reliability of SA design for embedded software.(3) In order to solve the problem of the transformation from real-time specifications to SA models of embedded software, an approach for transforming TCSP specifications to UML-RT models is proposed. TCSP (timed communicating sequential process) is a real-time extension of the process algebra CSP (communicating sequential process), which is fit for specifying real-time specifications of embedded software. Based on the transformation framework from requirements specification to SA models, TCSP is used in specifying the real-time specifications of embedded software, and UML-RT models are generated from TCSP specifications by a transformation mechanism which is established between TCSP and UML-RT. The instance shows the UML-RT models generated by this approach can increase the reliability of SA design for embedded software.(4) Aiming to the problem that the requirements specification of embedded software is difficult to take into account hard real-time requirements effectively, the process algebra support for hard real-time analysis is proposed. HTCSP (hard timed communicating sequential process) is proposed by extending hard real-time semantics on TCSP, it can be used to specify and verify the hard real-time dynamic behaviors of embedded system. A time optimal scheduling algorithm is proposed to be used in quantitatively analyzing and optimizing the hard real-time properties of embedded system. Moreover, the transformation from HTCSP specifications to UML-RT models is proposed.(5) Aiming to the problem that the requirements specification of embedded software is difficult to take into account resource requirements effectively, the process algebra support for multi-resources analysis is proposed. RCSP (resource communicating sequential process) is proposed by extending resource semantics on CSP, it can be used to specify and verify the resource dynamic behaviors of embedded system. Resource optimal checking algorithms are proposed to be used in quantitatively analyzing and optimizing the resource properties of embedded system. At last, the transformation from RCSP specifications to SA models is discussed.
|
PDF Full Text Request