Formal Hazard Analysis of Hybrid Systems in cTLA

Hybrid systems like computer-controlled chemical plants are typical safety critical distributed systems. In present practice, the safety of hybrid systems is guaranteed by hazard analysis which is performed according to procedures (e.g., HazOp) where experts discuss a series of informal argumentations. Each argumentation considers a specific required system property. Formal property proofs can increase the reliability. They, however, have often to deal with very complex hybrid systems. Therefore, methods are needed which structure and decompose formal verification tasks into manageable substasks. With respect to this, our approach achieves a relatively direct translation of informal argumentationsinto formal proofs. Since the informal argumentations mostly do not refer to the system as a whole but do only address specific parts and aspects, the formal proofs also can deal with partial, less complex system models. In result, even very complex systems can be verified in wellmanageable s...

• Type: Conference
• Year: 1999
• Where: SRDS
• Authors: Peter Herrmann, Heiko Krumm
• Keywords: Hazard Analysis, Hybrid Systems, Informal Argumentation, Operating Systems, SRDS 1999