Research On Real-time Systems Safety Verification Based On Temporal Fault Tree

The complexity of real-time systems is increasing together with its rapid development in critical information arears, to solve the problem of how can we guarantee the safety of real-time systems, keep them away from accident has become the emphasis in software engineering research. Nowadays, research on software safety analysis mainly focus on requirements specification and software functional design supported by fault tree analysis and functional modeling. However the two are separated in software development, which makes that on the one hand, analysis result from safety requirements can be hardly reflected to software design for guiding, on the other hand design model cannot ensure whether the software is safe because of the lack of safety requirements. The traditional fault tree analysis and the expended focus on safety requirements abstraction but do nothing on making sure whether the requirements are satisfied in system design. AADL(Architecture Analysis & Design Language) is able to describe the functional and nonfunctional attributes of systems, but it isn't able to find potential hazards because that it failed to describe the safety requirements.In this thesis, we propose a method for real-time systems safety verification based on TFT(Temporal Fault Tree), integrating safety requirements analysis and software functional design using model checking. It realizes the verification by ensuring that the safety requirements abstracted from TFT is satisfied in AADL model. The main contents of this thesis are as follows:Firstly, a framework combining safety attributes abstracted from TFT and system model described by AADL is provided for real-time systems safety verification.Secondly, substep confirmation is taken to ensure that safety attributes abstracted from TFT by using minimum cutset calculation is correct, so that the verification will be correct. It contents two parts: correctness verification of TFT building and consistency detection of specified attributes.Thirdly, the transformational rules between the subset of AADL and timed automata is provided for translation, after which system model from AADL to timed automata is generated, which can be verified under UPPAAL.Finally, a case study of PBA(Powerboat Autopilot) system is given and the method is proved to be viable and valid after achieving the verification step by step, so that a new thinking is provided.