Formal Hazard Analysis of Hybrid Systems in cTLA

9 years 6 months ago
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...
Peter Herrmann, Heiko Krumm
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where SRDS
Authors Peter Herrmann, Heiko Krumm
Comments (0)