In this chapter, we discussed some temporal logic semantics of fault trees, and presented an analysis of the role of temporal logic in FTA. Based on the analysis, we proposed a simple logic semantics for our FTA/OTS based on classical propositional logic and basic concepts of observational transition systems. Then we focused on how to link fault tree analysis to program development (system requirements specifications), demonstrated how to trans-form the fault tree specifications into trans-formal system specifications with OTS/CafeOBJ.
An analysis of the combination of the FTA/OTS and OTS/CafeOBJ was concluded in Section 6.3.4.
To our understanding, to ensure the correctness of the fault trees, providing an un-derstandable formal construction model as well as simple logic semantics is more efficient and better than the approach that first build the fault trees by intuition (in an informal way), and then verify its correctness afterwards by some complex logic semantics defined
for the fault trees. This is the main motivation why we further refine our formal fault tree model from temporal logic to the OTS model. Another motivation is inspired by Hansan’s work [HR98], that is, trying to link the fault tree analysis to program development by providing a common system model for both of them.
Hansan’s work contributes an approach from safety analysis (with FTA) to Software requirements based on duration calculus and interval temporal logic (ITL) for the inter-pretation of both fault trees and software requirements [HR98]. However, it does not discuss how to ensure the correctness of the fault trees and how to derive the concrete formal system specifications from the fault trees.
Another related work about the formal semantics and specifications of fault trees can be found in [CSD00] (D. Coppoit, K. J. Sullivan and J. B. Dugan, 2000), which presents an approach to write the formal specification of dynamic fault trees with Z specification language. However, as we known, Z itself is not an executable formal language, which limits its usage if we want to prove some safety properties based on the formal system (or fault tree) specifications. In addition, Coppoit et al. do not consider the decomposition problem with respect to the conjunct fault events because their attention is focused on the formal semantics of dynamic fault trees.
Some other formal works on fault trees mainly focus on the formal semantics (usually with temporal logic) of fault trees, such as [STR02, BA93], while as far as we know, none of them focus on how to connect the fault tree analysis with program development. And even with the temporal semantics of fault trees, some issues are still disputed as we dis-cussed in Section 6.1.
In a nutshell, thanks to the advantages and properties of OTS/CafeOBJ, our work presents an approach from safety analysis to program development (requirements specifi-cations and verifispecifi-cations), which makes engineers and designers from multiple disciplines work together more efficiently and effectively, and makes it possible to achieve more reli-able and efficient safety and requirements analysis.
Chapter 7 Conclusions
7.1 Contributions
This dissertation has developed techniques to achieve more reliable formal fault tree analy-sis as well as more efficient requirements analyanaly-sis. Three important issues have been ad-dressed, that is, the correctness of the fault trees, the combination of fault tree analysis and formal methods with CafeOBJ and Maude, and the transformation from the results of fault tree analysis into formal system specifications with OTS/CafeOBJ by using the common framework of OTS. The technical contributions of this dissertation can be con-cluded as follows.
1. It identifies decomposition of fault events as a core issue that guarantees the cor-rectness of the fault trees, i.e., the sub events must formally result in their top event through the given logic gate. And for solution, it proposes two formal fault tree construction models based on temporal logic and observational transition systems, respectively. The advantages of the formal fault tree construction models proposed in this dissertation are as follows:
• It (both of the two models) is a heuristic and deductive method to build fault trees more precisely and effectively;
• The correctness of the generated fault trees is proved by the construction process itself, rather than requiring a stand-alone verification, and thus avoid-ing the problems that often arise with traditional methods. At the same time, it gives designers and domain experts the ability to discover domain (transi-tion) rules and previously unnoticed design deficiencies during the construction process;
• It integrates (records) the domain (transition) rules into the fault trees, which makes the analysis more complete and is useful for revising and rechecking of the fault trees;
• The formal construction model based on classical propositional logic and basic concepts of OTS provides an alternative for engineers who are not familiar with temporal logic, and thus it complements the model of temporal logic one for different applications.
2. It presents a study on the combination of fault tree analysis and formal methods with CafeOBJ and Maude.
• It proposes an approach to derive concrete requirements (safety assumptions and commitments) from FTA so as to guild and assist the subsequent system design and verification;
• It demonstrates how to write fault tree specification and realize automatic calculation of minimal cut sets of fault trees with term rewriting system (TRS) of CafeOBJ;
• It demonstrates how to formally model, specify, and verify OTSs with CafeOBJ based on the analyzing results of FTA. And as a complement of theorem proving technique provided by CafeOBJ, it also demonstrates how to model-check OTSs with Maude (a sibling language of CafeOBJ).
3. Most important, it further proposes a novel formal fault tree analysis based on OTS. The point is that, by using a common framework of OTS, it is possible to use the results of fault tree analysis directly, when specifying and verifying the system with OTS/CafeOBJ. The transformation from fault tree specifications into formal system specifications with OTS/CafeOBJ is demonstrated. Therefore, it presents an approach to link safety analysis and requirements analysis in a consistent and smooth way, and it provides a common framework for engineers and designers from multiple disciplines to work together more efficiently and effectively.