Maurice Comlan
Published: 2016
Total Pages: 0
Get eBook
Les réseaux de Petri et leurs extensions constituent un formalisme très connu pour la modélisation de la spécification des systèmes à évènements discrets temps réel. Pour ces systèmes, les exigences de vérification et de validation sont indispensables pour garantir leur bon fonctionnement car la moindre erreur peut entrainer des conséquences catastrophiques. Pour analyser le comportement du système, il est courant de construire le graphe d'états (ou espace d'états) qui énumère de façon exhaustive les différents états accessibles.Ce graphe permet de vérifier des propriétés génériques comme le caractère borné, l'accessibilité, la terminaison, la vivacité, l'absence de blocage, etc. Mais la construction de cet espace d'états est confrontée au problème d'explosion combinatoire du nombre d'états lié à la complexité et à la concurrence du système.L'une des alternatives pour contenir cette combinatoire est de conserver uniquement les ordres partiels entre les évènements. Le dépliage est une technique d'ordre partiel adaptée à la vérification, au diagnostic et à la planification. Cette thèse contribue à l'étude du dépliage des réseaux de Petri et, plus particulièrement,apporte une contribution au dépliage des réseaux de Petri avec des arcs de reset. De plus, le dépliage explicite les exécutions possibles du système qui sont, par définition, des processus. Il s'agit plus précisément des processus de branchement qui diffèrent des processus classiques. Ainsi, nous proposons une algèbre adaptée aux processus de branchement issus du dépliage des réseaux de Petri.