Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4
What and Who
Partial Order Reduction for Model checking of Timed Systems
Marius Minea
Carnegie Mellon University, Pittsburgh, PA, USA
Talk
AG 1, AG 2, AG 3, AG 4
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 12 July 99
14:00
60 Minutes
46.1
022
Saarbrücken
Abstract
Timed systems have an increasing presence in applications where correct operation is essential, from specialized safety-critical systems to mass consumer products. Formal verification techniques face the challenge of the state space explosion problem, since the state space of concurrent systems grows exponentially with the numer of components. Timing conditions significantly increase this complexity, often exceeding the current capabilities of verification tools.
I will present how to alleviate this problem by using partial order reduction, a technique which has been successfully applied to the verification of untimed asynchronous systems. This method explores only a subset of representative trajectories in the state space, while preserving the verified property. The verified models are networks of timed automata, a formalism based on state-transition graphs augmented with continuous-time clocks. Specifications are given in an extension of linear temporal logic, in which timing relationships of events are modeled by specifying bounds on clock differences. I show how to extend and modify a relaxed local time semantics for timed automata in order to preserve properties in the selected logic. The resulting model checking algorithm achieves reduction in both the control state space and the time space of the model.
I will present how to alleviate this problem by using partial order reduction, a technique which has been successfully applied to the verification of untimed asynchronous systems. This method explores only a subset of representative trajectories in the state space, while preserving the verified property. The verified models are networks of timed automata, a formalism based on state-transition graphs augmented with continuous-time clocks. Specifications are given in an extension of linear temporal logic, in which timing relationships of events are modeled by specifying bounds on clock differences. I show how to extend and modify a relaxed local time semantics for timed automata in order to preserve properties in the selected logic. The resulting model checking algorithm achieves reduction in both the control state space and the time space of the model.
Contact
Tom Henzinger
0681/93 25-300/301
--email hidden
passcode not visible
logged in users only