J. Xiang, K. Futatsugi (Japan), and Y. He (PRC)
Software Engineering, Fault Tree Analysis, Formal Specifications, CafeOBJ
Most traditional formal fault tree analyses have focused on providing formal semantics for fault tree constructors; formal verification of the correctness of the fault tree is often done after the informal fault tree has been built by intuition. In this paper, based on an analysis of the harm that can be caused by these traditional methods, we propose a novel formal fault tree construction model in which the correctness of the fault tree is proved by the construction process per se, and domain rules are organically integrated into the fault trees for reverse checking. Furthermore, in order to provide engineers with a practical tool to write formal specifications, without the need for difficult and tedious logic deduction, we demonstrate how CafeOBJ, a wide spectrum specification language based on multiple logical foundations, can be used to write the formal specifications for fault trees.
Important Links:
Go Back
