Vers l'intégration de paramètres temporels statiques et dynamiques dans les techniques de vérification par ordre partiel

Les systèmes temps réels sont utilisés de nos jours d'une façon importante, surtout dans le domaine des applications critiques. Pour les modéliser, nous avons opté pour l'utilisation des réseaux de Petri temporels (TPN) qui sont une extension temporelle des réseaux de Petri simples (Rdp) proposés par Carl Adam Petri. Ce choix est justifié par le fait que les TPN sont des modèles permettant de représenter les aspects importants des systèmes temps réel comme la concurrence, la synchronisation et les contraintes temporelles d'une façon triviale. De plus, les TPN offrent des techniques formelles de vérification qui intègrent les contraintes temporelles. Parmi ces techniques, ce mémoire s'intéresse aux approches énumératives. Ces approches se basent sur des abstractions et visent à représenter les espaces d‘états infinis des TPN par des graphes finis. Plusieurs abstractions d'espaces d'états ont été proposées dans la littérature : le SCG (State Class Graph), le CSCG (Contracted State Class Graph), le ZBG (Zone Based Graph), etc. Ces graphes sont finis pour des TPN bornés (ayant un nombre fini de marquages accessibles) et préservent les marquages et les séquences de franchissement des TPN. Ce mémoire s'intéresse au CSCG car il est plus compact que les autres. Cependant, à l'instar des approches énumératives, le CSCG se heurte au problème d'explosion combinatoire. Pour atténuer ce problème, ce mémoire propose d'étendre et d'appliquer des techniques de réduction d'ordre partiel aux TPN. La première contribution de ce mémoire est d'implémenter une technique d'ordre partiel pour les TPN. Cette technique est une extension aux TPN de l'approche de réduction Stubborn Set (proposée par Valmari pour les réseaux de Petri simples). La deuxième contribution est le développement d'un outil qui permet de générer l'espace d'états réduit d'un TPN en appliquant notre technique. Cet outil permet aussi la construction des graphes SCG et CSCG. Nous avons réalisé certaines optimisations dans l'implémentation de cet outil en nous basant sur des algorithmes de classes d'états de moindres complexités. Nous avons testé l'approche d'ordre partiel proposée dans ce mémoire et comparée avec d'autres approches et variantes. Divers réseaux de Petri temporels ont été testés, incluant quelques modèles de références. Ces derniers sont utilisés pour confronter des outils de vérification, dans des compétitions organisées au sein de la conférence annuelle Petri nets. Les résultats obtenus en utilisant ces TPN de références montrent que notre technique permet d'avoir de meilleurs résultats par rapport aux autres approches en utilisant les même TPN. En effet, le gain a varié entre 20% et 90% en termes de nombres de classes d'états, d'arcs et de temps d'exécution.