Modeling, Specification and Verification of an Emergency Closing System

In this paper we present a realtime modeling technique which is based on a global clock architecture with a discrete time scale. We argue that this model can be applied to a wide range of scenarios. Furthermore we illustrate the modelling technique by an example describing an emergency closing system which is specified in the VSE tool.