|
|
 |
|
Jeudi 11 Février
| Heure: |
14:00 - 15:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Timed Aggregate Graph : a finite graph for model checking of Time Petri Nets |
| Description: |
Amal Chamakh Time Petri Nets (TPNs) are one of the most powerful formalisms for the
specification and the verification of systems involving explicit timing
constraints. To deal with model checking of timed systems modeled by TPNs, we
propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting
the behavior of bounded TPNs with strong time semantics. The main feature of
this abstract representation compared to existing approaches is the encoding
of the time information. This is done in a pure way within each node of the
TAG allowing to compute the minimum and maximum elapsed time in every path of
the graph. The TAG preserves timed traces and reachable states of the
corresponding TPN and allows for on-the-fly verification of reachability
properties. We also introduce an algorithm for a modular construction of the
TAG, to better confine the state explosion problem. |
|
|
