Georg Rock
In specifying industrial (sized) systems, we are often confronted with the problem of expressing realtime properties. In these applications we realized that these propositions are both hard to find and hard to prove. Those properties could be expressed in many specification languages as, for instance, MTL, TLA or VSE-SL. One of the main problems in this area is the complexity of timing constraints that could arise and the variety of situations which could appear in such a system. We try to overcome these problems by exploiting the advantages of hybrid systems and the VSE-II methodology.