MIT nyitóoldal
Térkép

Projects
   Actual
   Finished
   Complete list

Formal verification of safety requirements in fault tolerant systems

OTKA project
1999 - 2001

Local supervisor: Majzik István
Official project supervisor: BME MIT FTSRG

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 about the project:
Official homepage: http://www.inf.mit.bme.hu/FTSRG/Projects/otka_mi.html
Department homepage: http://www.mit.bme.hu/projects/fault99/
Official email address: majzik@mit.bme.hu