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.


Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch