5th International Workshop on
Formal Methods for Industrial Critical Systems
Berlin, April 3-4, 2000
Modelling and Analysing the Railroad Crossing in a Modular Way
One problem of modelling hybrid systems with existing notations of hybrid automata is that
there is no modular structure in the model. We introduce an extended modelling notation which allows the
modelling of a system as a hierarchical structure of modules. The modules are capable of communicating
through the elements of an explicitly defined interface. The interface consists of signals and variables
declared with different access modes. This paper describes a model of the railroad crossing example
and how to verify it. The current version of a tool for reachability analysis using the double description
method to represent symbolically the sets of reachable configurations is presented.
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