Research And Implemention Of Embedded Based On Model-Driven Verification And Software Product Line

The size and complexity of the embedded software grow constantly, for the reason that the rapid improvement of the computing power of processors, the rapid development of embedded technology, and the continuously expanding of the field of embedded system applications, which results in increasing time and costs on development. Therefore, how to develop embedded software fast and effectively become a serious problem. The world's largest software industry standards organization OMG (Object Management Group) proposed a model-driven framework MDA(Model Driven Architecture) development methodology in order to solve the above problems. MDA methodology divides software development process into two main phases:model-level and code level. Model is mainly responsible for the correctness of system design, so that only little cost will be needed to fix an error in existing software.Recently, tools for developing embedded-oriented software are transferring from the traditional code-based development environment to model-based development environment. A model-based embedded software production line should integrate model based development tools and other correlative tools, and hence, it covers the entire development process of embedded software, such as modeling, simulation, verification, code generation and testing. It is not only in line with the trend of embedded software tools, but also has the corresponding theoretical, technique, and product foundations.Model-driven verification is an important part of the Model-based embedded software product line, so the key part will have impact on the quality of the system and later work. If existing problems can be detected in earlier phase, it can save a lot of manpower and resources. Real-time performance is a key indicator of today's mainstream embedded real-time systems, which requires corresponding action to be completed in the legitimate time, and no overtime phenomenon. Therefore, it is necessary to verify the schedulability among the tasks to determine whether the real-time performance of systems meet the requirements. This formalized model validation method was firstly proposed by the Clark and Emerson, the basic principle is to test the system for establishing formal model, clarify the nature to be verified, and then use the algorithm to check whether the model meets the requirements or not.Based on development environment of model embedded software product line, this paper will put focus on research and solve the formal verification problems of models on the basis of it, and study the scheduling problem of real-time embedded model. Firstly, this paper will introduce background and significance of the model-based embedded software product line, analyze the current trends, and then illustrate the source of the subject of this paper and the contents of this paper. On this basis, the writer will present an overall Needs analysis of the model-based embedded software product line. In the following part, the writer will focus on introducing the design of SCT scheduling check tools, including the relevant definitions and rule of the system analyzed by SCT, and designing and implementing the two behavioral automata model of tasks. Under the premise, the writer will design and implement the scheduling and simulation algorithm of SCT. Based on LambdaPRO, this paper will integrate other correlative tools, achieve the entire development process of model-based embedded software product line, and use an example application to illustrate and validate this development process. Finally, by summarizing the study of the paper, the author gives prospect of future research and development.