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.

Abstract

Real time systems are widely used today especially in the field of critical applications. For modeling, we chose to use Time Petri network (TPN), which is an extension of simple Petri networks (Rdp) implemented by Carl Adam Petri. This is justified by the fact that TPN models are used to represent important aspects of real-time systems such as concurrency and synchronization in a simple way. Besides, TPN are rich in theories that have helped us to implement our technique. The two major issues of real-time systems are the obtaining of an infinite state space and the combinatorial explosion. To overcome the first issue, we have chosen the method of abstraction CSCG (Contracted State Class Graph). It is a method of abstraction which is applied to the TPN to get a finite state space representation. To address the second issue, we have extended partial order reduction technique "Stubborn Set" in the context of TPN. Note that the Stubborn Set method is a partial order reduction technique that aims to alleviate the problem of combinatorial explosion of the state space of simple Petri net i.e. without considering the time constraints. Therefore, our first contribution of our research is to participate to develop a partial order reduction technique extending the method Stubborn Set in the context of TPN. The second contribution is the development of a tool to generate the reduced state space of TPN by applying our technique. It also allows the construction of the state space using other techniques discussed in the chapter "literature review". We have performed some optimizations in the implementation of this tool based on algorithms with reduced complexity taken from the literature. To test our technique with our developed tool, we chose various examples of temporel Petri nets such the benchmark TPN. The results shows that our technique can achieve better results compared to other techniques in terms of the number of state classes, arcs and execution time.