Research On Model Driven Safety Verification For Embedded System Designs

In recent years, the rapid enlargement scale of the embedded system and the software and the rapid increase of the systems’ complexity bring major challenges to the guarantee for the embedded system and software safety in the field of safety critical applications(such as aviation, transportation, nuclear power plant, etc.).At the same time, model driven system/software development technologies in the field of safety critical engineering begin to get wide attentions and applications. Traditional unified modeling languages(such as UML and Sys ML, etc.) have been more and more applied in the system and software modeling, but when facing safety critical areas these modeling languages and methods still have some problems at present, such as: the lack of elements and mechanisms which are used to describe the real-time embedded system’s nonfunctional behaviors(including effective modeling for time, resources and probability, etc.).Modeling languages still lack precise definition for model semantics, which brings difficulties for using these software models for the safety of the formal validation and analysis and so on.This paper mainly works on the safety analysis of the embedded system model,which is developed under the model driven architecture(MDA), and explores the safety analysis and verification methods for the Sys ML/MARTE state machine, Alta Rica model and the UPPAAL timed automata model which are based on model transformation. It includes the following sections:(1) Study the modeling problem of complex embedded system design which is based on Sys ML/MARTE; System modeling language Sys ML is a standard modeling language for the system engineering application development, while MARTE is mainly from the non-functional properties such as time constraints, the allocation of resources etc. to do modeling and analysis for the embedded system. In this paper in order to model the complex embedded systems’ behavior we mainly use Sys ML state machine model as a typical study object, which is combined with MARTE including semantic extension of nonfunctional resources such as time, probability.(2) As for a central problem of MDA: Model transformation is carried out which is based on the platform of AMMA for the conversion method between heterogeneous models, including: Establish Sys ML/MARTE state machine meta-model, Alta Rica meta-model and timed automata meta-model, and the semantic mapping relationships between them. Then use model transformation language ATL which is based on AMMA platform to construct model transformation rules. As a result, providing bases for the transformation which is from Sys ML/MARTE state machine model respectively to Alta Rica model and timed automata model, and the transformation is implemented under the model driven architecture.(3) Study the safety analysis and validation method for Sys ML/MARTE state machine model which is about time properties.Through Semantic mapping relationship between meta-models, which can be used to convert the Sys ML/MARTE state machine model to timed automata model, the needed temporal logic formula properties can be obtained from the Alta Rica model, then use analysis tool UPPAAL to do safety analysis and verification.(4) Study the safety analysis and validation method for Sys ML/MARTE state machine model which is about probability attributes; Including: do model transformation from Sys ML/MARTE state machine to the Alta Rica model, then generate fault tree model; after that let the fault tree be the fault tree analysis tool XFTA’s input, as a result, the systems’ safety analysis and validation can be carried out.(5) Designed a framework based on models which is for the embedded system design and analysis, and do modeling and analysis validation by respectively introducing the Aircraft landing instance modeling and the brake control system in the ARP4751.