Improving the verification of timed systems using influence information

Abstract

The parallel composition with observers is a well-known approach to check or test properties over formal models of concurrent and real-time systems. We present a newtechnique to reduce the size of the resulting model. Our approach has been developed for a formalism based on Timed Automata. Firstly, it discovers relevant components and clocks at each location of the observer using influence information. Secondly, it outcomes an abstraction which is equivalent to the original model up to branching-time structure and can be treated by verification tools such as KRONOS [12] or OPENKRONOS [23]. Our experiments suggest that the approach may lead to significant time and space savings during verification phase due to state space reduction and the existence of shorter counterexamples in the optimized model. © Springer-Verlag Berlin Heidelberg 2002.