Framework for the Hazard Analysis of Hybrid Technical Systems

A framework facilitating the formal specification of hybrid technical systems and the formal verification of certain properties preventing the occurrence of hazards is proposed. The framework consists of

• specification elements for modelling hybrid systems, hazards, and desirable system properties
• implication theorems to support the verification of specification elements

The specification elements are divided into different sections:

• System components facilitating constraint-oriented specifications of hybrid systems. The system components are further split up in groups modelling continuous components (vessels, pipes, ...), actors (valves, heatings, ...), sensors, and discrete components (computer control elements).
• Hazard descriptions enable the specification of technical hazards like leaking valves and blocked pipes.
• Property descriptions model desirable properties of the plants (e.g., the pressure in a vessel does not exceed a certain value; if the temperature of a fluid exceeds a value; there is no flow through a pipe anymore; ...).

An implication theorem states that a subsystem of a plant consisting of system components, hazard descriptions, and property descriptions, fulfill a certain property description. Thus, one can prove by using the theorems that a plant fulfills certain safety properties. (The verifications of the theorems are sketched in the theorem descriptions.)

The use of the framework is outlined by means of some example specifications.

If you are interested in further information, feel free to contact me