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.

Abstract (AI English translation)

Information popover about translation disclaimer

Verification by state space exploration (model-checking) is an effective technique for verifying properties on systems. Several verification tools use this technique through specifications expressing the behavior of the systems considered. These specifications represent models on which we can verify certain properties. Other verification tools, using the same technique, operate on the description of systems by acting directly on the source code.

Our work is generally inspired by the verification technique proposed by Godefroid in his VERISOFT verification tool. We propose the application of this technique on parallel systems by acting on the source code describing these systems. To do this, you must first adopt a technique allowing you to construct the state space of a system from its description in the programming language. Then, we apply a state space search algorithm to check certain properties. In our case, the systems to be verified as well as the verification tool are written in the JAVA programming language.