Andreas Nonnengart, Georg Rock, and Werner Stephan, German Research Center for Artificial Intelligence, Ltd., Germany
In formally analyzing and developing industrial sized systems we are often confronted with the problem of expressing realtime properties. Especially in safety critical applications as, for example, in embedded systems or in control software these properties are crucial for the right functioning of the systems. There are numerous suitable approaches that allow us to specify realtime properties: MTL, TLA or VSE-SL to name a few, and also there are various tools available to formally develop such systems. But in most cases the approaches are trimmed for their own highly specialized application area. We try to overcome this restriction by exploiting the advantages of a (fairly general) formal development tool like VSE-II and the rather specialized Hybrid Automata by combining these two approaches.