Application de la méthode de vérification de modèles sur des protocoles de communication JAVA

Abstract

La vérification par exploration d'espace d'états (model-checking) est une technique efficace pour vérifier des propriétés sur des systèmes. Plusieurs outils de vérification utilisent cette technique par l'intermédiaire de spécifications exprimant le comportement des systèmes considérés. Ces spécifications représentent des modèles sur lesquels nous pouvons vérifier certaines propriétés. D'autres outils de vérification, utilisant la même technique, opèrent sur la description des systèmes en agissant directement sur le code source. Notre travail est généralement inspiré de la technique de vérification proposée par Godefroid dans son outil de vérification VERISOFT. Nous proposons l'application de cette technique sur des systèmes parallèles en agissant sur le code source décrivant ces systèmes. Pour ce faire, il faut préalablement adopter une technique permettant de construire l'espace d'états d'un système à partir de sa description dans le langage de programmation. Ensuite, nous appliquons un algorithme de recherche dans l'espace d'états permettant de vérifier certaines propriétés. Dans notre cas, les systèmes à vérifier ainsi que l'outil de vérification sont écrits dans le langage de programmation JAVA.