Verifying the Safety of Formal Specification Using Fault Tree Analysis and Animation - Wen Jiang; Shaoying Liu (IEEE Access, 2025)
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.