Master Thesis - Past Projects - Abstract
A tool for automatic formal analysis of fault tolerance
The use of computer-based systems is rapidly increasing and such systems can now be found in a wide range of applications, including safety-critical applications such as cars and aircrafts. To make the development of such systems more effective, there is a need for tools for automatic safety analysis, such as analysis of fault tolerance.
In this thesis, a tool for automatic formal analysis of fault tolerance was developed. The tool is built on top of the existing development environment for the synchronous language Esterel, and provides an output that can be visualised in the Item toolkit for fault tree analysis (FTA). The development of the tool demonstrates how fault tolerance analysis based on formal verification can be automated. The generated output from the fault tolerance analysis can be represented as a fault tree that is familiar to engineers from the traditional FTA analysis. The work also demonstrates that interesting attributes of the relationship between a critical fault combination and the input signals can be generated automatically.
Two case studies where used to test and demonstrate the functionality of the developed tool. A fault tolerance analysis was performed on a hydraulic leakage detection system, which is a real industrial system, but also on a synthetic system, which was modeled for this purpose.
Keywords: Dependability, Fault Tolerance, Esterel, Formal
Verification, System Safety
Author(s): Markus Nilsson
Contact: Simin Nadjm-Tehrani
Click here to return.