Distributed construction of state spaces for an efficient verification of untimed systems

De nos jours, les applications basées sur les graphes sont largement répandues, en particulier avec la croissance des nouvelles technologies, notamment les applications mobiles, Le World Wide Web, les réseaux sociaux et l’internet des objets. Les applications mobiles sont des exemples où les graphes deviennent dynamiques et de plus en plus larges. Les graphes ne sont pas seulement limités à Internet, le Model checking est un autre exemple important. En effet, le model checking est une technique de vérification automatique des systèmes complexes qui nécessite un graphe modélisant ces systèmes comme une entrée pour fonctionner. Cependant, la taille de ce graphe d’entrée a tendance à être très large en fonction de la complexité du système, ce qui entraîne le problème de l’explosion combinatoire d’espace d’états. Ainsi, dans le cas des systèmes très complexes, le graphe devient difficile à générer et à stocker sur une seule machine en raison de la limitation de capacité matérielle. Les travaux présentés ici proposent deux types de solutions pour traiter plus efficacement des espaces d’états de plus large taille. La première s’appuie sur des ressources parallèles avec des techniques basées sur des algorithmes génétiques et la deuxième traite plus efficacement des diagrammes de décision binaires, en les adaptant au problème de la distribution de l’espace d’états.Nowadays, the application of graphs is widely spread especially with the growth of new technologies. World wide web and social networks are examples of such applications where graphs are becoming dynamic and going larger and larger. Large graphs are not only limited to internet, model checking is another important example likewise. Indeed, the model checking is an automatic technique used to check systems. This technique requires a graph modeling the system as an entry to operate on. However, the size of this entry graph has a tendency to be huge according to the system complexity which results the problem of state space explosion. In fact, in the case of very complex systems, the graph becomes hard to be generated and stored on the same machine because of hardware capacity limitation. The work presented here offer two types of solutions to deal effectively with large state spaces. The first relies on resources parallel cluster computing with techniques based on genetic algorithms. The second proposed deal more effectively with binary decision diagrams by adapting them to the problem of state space distribution