Font Size:

Program

Program

Abstract from Keynotes

Modeling, Verification and Application of Explicit Time Models

Timed models are obtained by adding an explicit notion of time to classical models like finite automata or Petri nets. In such models, quantitative properties can be expressed, for instance about delays between actions.

This feature makes them closer to "real" systems and, due to powerful decidability results proved in the nineties, they have been extensively studied during the last fifteen years in the framework of verification and control. Specific data structures and algorithms have also been proposed, leading to the development of "timed model-checking" tools, which have been applied to numerous case studies. We present in this talk a survey of these different aspects : modeling with explicit time, déciding the verification of timed properties and applying the results to practical cases.

Time Petri Nets Analysis with the TINA toolbox

TINA (TIme Petri Net Analyser) (www.laas.fr/tina) is a software environment to edit and analyse Petri Nets possibly enriched with priorities, time constraints, stopwatches and external data.

The toolbox offers the usual editing and analysis facilities (marking reachability sets, coverability trees, semi-flows), various abstract state space constructions, a step-by-step simulator and a model-checker for an enriched version of State/Event-LTL, a linear time temporal logic supporting both state and transition properties.

The abstract state space constructions preserve specific classes of properties of the concrete state spaces of the nets. Those properties may be general properties (reachability properties, deadlock freeness, liveness), specific properties relying on the linear structure of the concrete space state (linear time temporal logic properties, test equivalence), or properties relying on its branching structure (branching time temporal logic properties, bisimulation).

For Petri nets, these abstractions help preventing combinatorial explosion and rely on so-called partial order techniques. For Timed models, that have in general infinite state spaces, they provide finite representation of their behavior, in terms of state class graphs.

Top