Verifying the Safety of Formal Specification Using Fault Tree Analysis and Animation

Formal specifications can effectively guide the implementation of intended functionalities and improve the quality of software during its creation phase. However, a remaining challenge is how to verify the system’s formal specification to ensure its safety. In this paper, we describe a systematic approach that integrates fault tree techniques and animation technique to address this issue. Our method offers new ways to: (1) define the safety of processes, (2) establish a comprehensive set of rules that can effectively construct fault tree structures and reasonably integrate animation technique into this framework, and (3) propose a new algorithm for generating animation data for numeric type variables. We discuss these contributions and present a case study to demonstrate how our method can be applied in practice. We also report an experiment on applying our method to an automatic overtaking system to validate this technique.