Abstraction et analyse de l'espace des états des réseaux de Pétri temporels
Institution:
Paris 13Disciplines:
Directors:
Abstract EN:
Time Petri nets (TPN models) allow the specification of real-time systems involving explicit timing constraints. The main challenge of the analysis of such systems is to construct, with as few resources (time and space), a coarse abstraction preserving timed properties. We propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behaviour 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 time elapsed in every path of the graph. The TAG preserves runs and reachable states of the corresponding TPN and allows for verification of both event- and state-based properties. In the second contribution, we propose the appropriate algorithms for checking TCTL formulae and prove the correction of these algorithms.
Abstract FR:
Les réseaux de Petri temporels sont largement utilisés pour la spécification des systèmes où le temps est exprimé explicitement. Le principal défi pour l’analyse de tels systèmes est de pouvoir construire une abstraction finie de l’espace d’états qui préserve des familles de propriétés que l’on veut vérifier. De plus, les algorithmes de construction doivent être optimaux en termes de temps de calcul et d’espace mémoire. Notre première contribution dans cette thèse est un nouveau graphe appelé Graphe des Agrégats Temporisés (TAG) qui permet l’abstraction du comportement des réseaux de Petri temporels bornés avec une sémantique de tir forte. Le principal apport de notre approche, comparée aux approches existantes, est l’encodage des informations temporelles. En effet,chaque noeud du TAG comporte des informations temporelles permettant de calculer les délais minimum et maximum écoulés sur chaque chemin du graphe. Le TAG est fini pour les réseaux de Petri temporels bornés, et permet de préserver les séquences et les marquages accessibles ainsi que la vérification des propriétés sur les événements ou sur les états. Nous proposons dans la deuxième contribution des algorithmes pour la vérification des formules TCTL et prouvons leur correction.