ISSE

Search

FORMOSA


Start date: 23.03.2005
Funded by:
Local head of project: Prof. Dr. Wolfgang Reif

Abstract

 

Description

Uni Augsburg

FORMOSA

(integrating FORmal MOdels and Safety Analysis)

Summary

The goal of the FORMOSA (Integrating FORmal MOdels and Safety Analysis) project is to establish a method for the systematic development of formal models for high assurance systems. The aim is to reduce errors in requirements definitions of software based safety critical systems. This is achieved by combining formal models with safety techiques from engineering. Formal specifications are used to describe the system model and to formulate and verify safety properties. Design errors and safety flaws are detected by safety analysis techniques. The project investigates the theoretical foundations, an integrated methodology, and provides tool support (sponsored by DFG, German Research Foundation, DFG research programme `Integration von Techniken der Software-Spezifikation für ingenieurwissenschaftliche Anwendungen').

Motivation and Goal

The goal of this projects is a methodology for developing safety-critical systems. This goal is being achieved by combining well-known techniques and practices of safety analysis with state-of-the art formal methods. Formal methods allow to precisely describe systems and to rigorously prove (safety) properties. Safety analysis techniques on the other hand are very useful for detecting weaknesses in design and to provide safety approximations. The combination yields mutual benefits:

  1. Formal methods profit from new proof obligations, which are found by means of safety analysis.
  2. The significance of the results of safety analysis is enhanced, as formal proofs allow rigorous reasoning.
  3. The combination of both techniques leads to systems, which are both: functionally correct and fault-tolerant.

The project program spans theoretical foundations, methodological guidelines and a prototype implementaion. The results are demonstrated in two real world case studies: the "Funkgesteuerter Bahnuebergang" and the "height control of the Elbetunnel in Hamburg".

Integrated Methods

In the ForMoSA project different techniques from formal methods and safety engineering have been combined. The well-known fault tree analysis (FTA) has been enhanced with a formal semantics. The idea is to assign a temporal logic formula to every gate in the fault tree. This leads to five new types of fault tree gates. The formal semantics allows to rigorously prove the completeness of a fault tree. It has been shown, that cut sets found with a formal fault tree analysis have the same semantics as those found by an informal technique (minimal cut set theorem). As a next step failure modes and effects analysis(FMEA) and FTA have been combined in a universal safety analysis method - deductive cause consequence analysis (DCCA). This methods span - as special cases - the verification of functional correctness, FMEA and FTA.

System models

For safety analysis with formal methods new system models must be developed. Traditionally formal models only represent intended behavior. (Hardware-)Failures are not part of the model. Therefore a method for integrating hardware failures in a given formal model was developed. In this context another problem must be solved: How can failure modes be found and specified formally? This topic is adressed with a new safety analysis technique - failure sensitive specification. It allows to prove - with respect to the systems' boundaries - if all possible component failure modes have been taken into account and if a given failure mode has been integrated in the system model correctly or not.

Quantitative Extensions

All developed methods can be enhanced with a quantitative extension. In the case of formal FTA and DCCA this approach is analogous to quantivative FTA in the traditional sense. During the project it became apparent, that in general advancements can be made here. Traditionally qualitative and quantitative analysis are completely separated. In particular all configuration parameters of the system are chosen at time of the analysis and afterwards these parameters are used for quantitative approximations. It many practical applications the results of qualitative (formal) safety analysis are not dependent on the choice of some free parameters (which are used i.e. for configuration of the system). In these cases the free parameters can be kept throughout the whole safety analysis process. This allows to use optimization techniques to find the best konfiguration of the system. Together this method is called safety optimization.