Hierarchical Verification of Reactive Systems with Timing Constraints

Abstract:- The paper describes model checking for reactive systems with timing constraints. Model of the system to be verified is given in Statecharts visual language. Timing constraints can be assigned to the states of the system. Required properties of the system can be given as system invariants and/or formulas of the branching-time temporal logic. Timing requirements are incorporated in a formula using bounded temporal operators. The proposed hierarchical verification algorithm works on-the-fly without constructing the flat state-transition graph. If the property does not hold, the counter-example can be found without searching the entire state space. Key-Words: