5th International Workshop on
Formal Methods for Industrial Critical Systems
Berlin, April 3-4, 2000
Modeling and Verifying a Temperature Control System using Hybrid Action
Systems
We formally describe and verify a real-time temperature control system for a nuclear
reactor tank, using a generalization of action systems to hybrid systems (based on weakest
precondition predicate transformer semantics) as our formal framework. The analyzed control system
is a linear hybrid system, combining discrete control with continuous dynamics. Our work can be seen
as a case study on the applicability of the hybrid action system formalism to study the reachability
problem, i.e., to prove that an unsafe state can not be reached by executing the system.
Note: The content of the following files is part of
GMD Report No. 91
and subject to its copyright.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch