Randomised exploration of large state spaces for verification
Exploration randomisée de larges espaces d'états pour la vérification
Résumé
Nowadays, the automated systems are omnipresent: industrial processes, avionics, atomic energy... The presence of such systems in critical applications, coupled to their complexity makes essential their checking in an automatic way in order to guarantee the safety of their operation. Moreover, the economic constraints impose a short time of development, which makes increased the need for effective checking methods at reduced cost. The Model-Checking algorithms are designed for the total checking of systems by traversing their state graphs. However, the state graphs of real software systems have very big sizes (combinatory explosion of the size of the state space). This phenomenon constitutes the principal obstacle of the automatic checking by model checking. Alternatively, one recourse to the partial exploration via ranomized algorithms. Instead of giving up the exploration because of lack of resources and not to return any answer about the validity of the system, the result of the checking is given roughly with an error probability that one can control. The majority of the randomized methods of checking use random walk as exploration scheme. The methods which we propose operate on the scheme even of the exploration as well as the replacement techniques in memory to bring important performances. These algorithms present a rather complete play of exploration strategies: in-depth, in breadth, or alternatively according to a predefined mixing parameter. The choice of this parameter is guided by a density factor DF that characterizes the considered graph.
De nos jours, les systèmes automatisés sont omniprésent : processus industriels, avionique, énergie atomique... La présence de tels systèmes dans des applications critiques, couplée à leur complexité rend indispensable leur vérification de façon automatique afin de garantir la sûreté de leur fonctionnement. En plus, les contraintes économiques imposent un temps de développement court, ce qui rend accru le besoin de méthodes de vérification efficaces et à coût réduit. Les algorithmes de Model-Checking sont conçus pour la vérification totale des systèmes en parcourant leurs graphes d'états. Cependant, les graphes d'états des systèmes logiciels réels ont de très grandes tailles (explosion combinatoire de la taille de l'espace d'états). Ce phénomène constitue l'obstacle principal de la vérification automatique par model checking. Alternativement, on a recours à l'exploration partiel via des algorithmes randomises. Au lieu d'abandonner l'exploration par manque de ressources et ne retourner aucune réponse quant à la validité du système, le résultat de la vérification est donné approximativement avec une probabilité d'erreur que l'on peut contrôler. La majorité des méthodes randomisées de vérification utilisent la marche aléatoire comme schéma d'exploration. Les méthodes que nous proposons opèrent sur le schéma de l'exploration même ainsi que sur le remplacement en mémoire pour apporter des performances importantes. Ces algorithmes présentent un jeu assez complet de stratégies d'exploration: en profondeur, en largeur, ou alternativement selon un paramètre de mixage prédéfini. Le choix de ce paramètre est guidé par un facteur de densité DF caractéristique du graphe considéré.
Loading...