Research On Verification Methodology About System Safety Design Based On AltaRica Model

With the rapid development of computer technology, embedded system has been widely used in the safety critical field such as medical treatment, transportation communication, aeronautic and astronautics. How to improve system safety and prevent catastrophic accident has been an hot topic in the field of software engineering. AltaRica is a kind of modeling language, which describes the behavior of a system in a normal case and in the presence of failures at the same time. The research on system safety based on AltaRica model is still hotspot. Although there are a few tools for system safety analysis using AltaRica model, for exhausting analysis and temporal property verification, tool support is still lack. SPIN remains advantages for exhausting analysis of modeling and verification of line temporal logic, which is a mature model checking tool. However, SPIN cannot verify AltaRica model directly.For above problems, in this thesis, we transform AltaRica model to Promela model, meanwhile, specify safety requirements by LTL, and then use SPIN to verify and analyze Promela model. Finally, we trace the design deficiency of AltaRica model with the result of verification and traceabilty information model. The main contents of this thesis are as follows:Firstly, we propose transform rules of AltaRica model,which transformed to Promela model on the basis of semantic analysis of AltaRica model and Promela model, and give formal proofs about the semantic equivalence of AltaRica model and Promela model. Specifying safety requirements using LTL, safety requirements specification and Promela model formalized verification using model checking tools. Meanwhile we also propose system safety design verification method based on AltaRica model.Secondly, with features of the model checking verification result, we give the traceability information model, which map the verification result to the design deficiency of AltaRica model. Building the meta-model of verification result traceability information model, then instances it according to trace target. Designing traceback algorithm based on traceability information model. It has realized automatic trace of verification result to the design deficiency of AltaRica model even to safety problem of system or component.Thirdly, for the proposed system safety design and verification methodology based on AltaRica model, we design and implement the prototype tool A2 STool. We illustrate the function modules of A2 STool, then give the design framework and the execution process of the tool and the key technology of realization.Finally, a case study of wheel brake system control unit is given. It gives integrated transformation from AltaRica model to Prolema model using prototype tool, safety requirements specification and Promela model formalized verification using model checking tools(SPIN). It has also discovered the deficiency of system design using traceability information model in accordance with the verification result. Hence, demonstrate the validity and feasibility of the proposed method. Our approach provides a new idea for the system safety analysis.