Formal verification of safety requirements in fault tolerant systems

Sponsors:

OTKA F030553 (Hungarian Scientific Research Fund)

Period:

Jan 1, 1999 – Dec 31, 2001

Participants:

István Majzik, Gábor Huszerl, Ph.D. students (Technical University of Budapest, Department of Measurement and Information Systems)

Project aim:

Computer systems with high safety requirements are extensively used in our everyday life (e.g. traffic control systems, power plants). The high level of dependability these systems require is hard to be assured, due to unavoidable component faults and accidental conceptional failures in the design process. Accordingly, it is necessary to (i) incorporate fault tolerance mechanisms in the system and (ii) verify the properties of the design by using mathematical formalisms. The formal verification of fault tolerant systems poses the problems of fault modeling, fault classification and error coverage.
The project aims at the formal verification of safety properties in computer systems designed using the Unified Modeling Language (UML). Extensions of the standard language are elaborated which allow the designer to describe faulty behavior, the applied fault tolerance structures, as well as the safety requirements. The verification procedure should be able to prove that the fault tolerant system satisfies these requirements, also in the case of the (anticipated) component faults.

The deliverables can be grouped in the following three main categories:

Extensions of UML required for modeling safety critical fault tolerant systems,

Formal verification of UML designs,

Integraton of the verification procedures into an UML-based CASE tool.

Further information:

István Majzik

 

---