Spin model checker

Plus les programmes se complexifient, faisant appel à de nombreuses méthodes, bibliothèques et frameworks, plus ils deviennent difficiles à debugger, maintenir et améliorer. De ce fait, les projets de développement échouent à se réaliser dans le temps planifié par manque de moyens, de ressources, et du fait de la complexité croissante des projets. Pourtant il est impératif pour les projets critiques de veiller à la bonne qualité du logiciel, à sa facilité de maintenance et à sa sûreté de fonctionnement (surtout dans le domaine médicale, nucléaire, bancaire, militaire, aérospatial et des transports). Cela passe essentiellement par l'utilisation d'outils de vérifications, de modélisation et de tests.

Les outils de vérification et de validation logiciel se répartissent en trois groupes : celui des tests unitaires – à charge au testeur d'écrire les jeux de tests qui couvrent tout ou partie du code –, celui des vérificateurs de preuve formelle – le développeur doit annoter le code source avec des formules de spécification formelle –, et celui des model-checkers – pour lequel le système doit être décrit par un modèle générique, dans un langage spécifique au model-checker, pour être vérifié et validé par celui-ci.

Les outils de tests unitaires, non-intrusifs, sont bien implantés dans le milieu industriel et sont souvent intégrés dans les IDE, puisqu'ils ne viennent pas modifier la façon académique de réaliser les logiciels (codage, compilation, linkage, débogage...), les tests pouvant même s'effectuer en dehors de la phase de codage (tests de bibliothèques). En revanche, ils sont limités et ne peuvent couvrir l'ensemble des cas possibles du programme (par exemple, pour couvrir l'ensemble des possibilités d'une simple variable entière sur 32 bits (un int32) il faudrait 232 tests). Cependant, avec une bonne couverture de code, on obtient rapidement une qualité de code satisfaisante.

Les vérificateurs de preuves formelles (Interactive Theorem Provers) sont davantage restreints au milieu de la recherche, car ils requièrent des compétences spécifiques, une maîtrise des langages de spécifications algébriques et d'outils qui ne sont pas, pour la plupart, industrialisés. Une méthode bien différente de la programmation classique puisqu'il s'agit non plus de coder des instructions mais de spécifier mathématiquement comment doit se dérouler le programme. Si toutes les spécifications sont validées, le programme est prouvé comme étant sûr. Certains logiciels de preuves formelles peuvent générer le code source final à partir des spécifications (AtelierB, Isabelle, ACL2) tandis que d'autres s'utilisent par annotation du code source (Frama-C et ses extensions Jessie et Wp). Cependant, la preuve formelle est une méthode qui gagne en influence, notamment avec l'utilisation de pré-conditions et post-conditions comme dans la modélisation UML avec OCL (Object Contraint Language) et la programmation par contrats. [1, 4, 5, 6, 7]

Quant aux model-checkers, ils se situent dans un groupe particulier, car ils sont complètement indépendant du programme source. Il s'agit de modéliser une partie du programme, dans un langage générique qui peut modéliser tout type de systèmes et de valider la cohérence du modèle. C'est très utile par exemple pour les applications multi-threads ou multi-process, pour valider que la communication inter-processus ne va pas se terminer en inter-blocage (deadlocks) ou autres défaillances.

Difficile à tester par les tests-unitaires et les preuves formelles, les model-checker nous permettent de modéliser facilement les threads ou process, leurs ressources et leurs communications, puis de valider tout les cas d'exécutions. Par ailleurs, ils permettent également de s'abstraire de la complexité des programmes sources codés en langages impératifs. En revanche, il ne s'agit que de modèles et n'ont pas vocation, pour la plupart, à générer le code source du produit final. Ils servent donc à modéliser et valider les systèmes complexes et nonseulement les programmes informatiques, mais également les systèmes électroniques, mécaniques ou tout systèmes de type état-transitions. On les retrouvent souvent dans l'industrie quand il s'agit de modéliser du matériel électronique, des protocoles de bas-niveau ou des applications de contrôle. Certains model-checkers comme Spin ou SMV sont même intégrés dans des systèmes de CAO (Conception Assisté par Ordinateur, ou CAD, Computer-Aided Design) pour améliorer la fiabilité. Par contre les model-checkers ne peuvent pas, ou difficilement, modéliser des systèmes non-finis utilisant des fonctions récursives ou des données externes en entrée (une solution est de les modéliser au préalable), et ils sont également limités en espace d'états qu'ils peuvent gérer (une possibilité est alors de les scinder en plusieurs sous-modèles). [2]

Spin est un précurseur et également l'un models-checker les plus cités dans la presse. Développé à partir de 1980 par Gerard J. HOLZMANN pour modéliser les protocoles de communication, au sein du groupe Unix du Computing Sciences Research Center du laboratoire Bell (inventeurs, avec en particulier Dennis RITCHIE et Ken THOMPSON, du langage C, du système Unix, du langage Awk, du système Plan 9, du format UTF-8). Il a été rendu publique et open-source en 1991 et est aujourd'hui considéré comme l'un des plus puissants model-checkers disponible. De plus il est également relativement simple à utiliser grâce à son langage Promela (PROcess Meta Language).[3]

Dans la suite de cet article, nous allons modéliser quelques petits programmes multi-threads et multi-process avec Spin, les vérifier et les valider.

1. Installation

Spin analyse les modèles écrits en langage Promela, les vérifie et les valide. Il s'exécute en console mais il existe également des interfaces graphiques, tel que iSpin, xSpin et jSpin. Dans cet article, nous utilisons l'interface iSpin.

Sur la site officielle de Spin, en suivant la rubrique installation, on trouve le paquage gzip à décompresser, spin625_linuxXX.gz, XX suivant le type d'architecture. Pour ces tests, nous utiliserons la version 6.2.5 du 4 mai 2013. [9]

Après décompression (gzip -d) on renomme spin625_linuxXX en spin, on ajoute les droits en exécution et on le déplace dans le répertoire /usr/local/bin. Ça peut paraître assez basique comme installation, mais il n'y aura que deux fichiers, spin et ispin, à installer.

Pour ajouter l'interface iSpin, installez au préalable la bibliothèque Tcl/Tk (présente en principe dans toutes les distributions GNU/Linux), de façon à ce que la commande wish ouvre une fenêtre Tk et un terminal Tcl. Téléchargez ensuite le fichier ispin.tcl (ou récupérez-le du tarball source), renommez-le en ispin avec droit en exécution et placez-le dans le répertoire /usr/local/bin. La commande ispin devrait vous ouvrir l'interface graphique, un peu fruste mais rapide et robuste, avec l'onglet d'édition prêt pour votre premier modèle Promela.

2. Exemples

2.1 Bonsoir et bonne chance

L'interface se compose de plusieurs onglets, Edit/View pour éditer le modèle en Promela et vérifier la syntaxe, Simulate/Replay pour lancer la simulation, Verification et Swarm Run pour les analyses et la validation, Help pour ouvrir une fenêtre d'aide, puis les boutons de gestion de session.

2.1.1 Dans le désordre

Pour un premier modèle, on va juste tenter d'afficher de deux parties d'un message dans l'ordre. Pour ce faire, nous aurons besoin de deux processus, que l'on modélise par des bloc active proctype (l'instruction active pour le lancer au démarrage). En ce qui concerne l'affichage, la fonction printf de Promela s'utilise comme celle du C. D'ailleurs la syntaxe général du langage Promela est assez proche de ce dernier, on y retrouve les mêmes accolades, parenthèses, opérateurs et comparateurs mais les similitudes s'arrêtent là.

Dans l'onglet Edit/View on écrit le programme suivant :

Avant de pouvoir simuler le code source, sauvegardez-le dans un fichier (bouton Save As...), de préférence avec l'extension .pml, pour Promela. Ce fichier sera nécessaire pour la suite.

Faites ensuite un Syntax Check, pour une vérification syntaxique. Si rien n'est à signaler, passez à l'onglet Simulate/Replay et cliquez sur le bouton (Re)Run. Si tout se passe bien, vous devriez voir apparaître le résultat de la simulation.

Que l'on modélise un thread ou un processus, on utilise la même instruction proctype. En effet, au niveau du modèle, proctype s'applique aussi bien à un processus, qu'à un thread, un automate, une machine à café ou tout autre acteur du système d'information que l'on souhaite modéliser.

Cependant, les processus activene se lancent pas forcement dans l'ordre et l'on peut avoir un résultat incohérent lorsqu'on se place en mode interactif (onglet simulation) et que l'on démarre par le processus pChance.

2.1.2 Dans l'ordre mais...

Pour contraindre l'ordre d'affichage des messages, nous utiliseront un sémaphore, l'un des moyens de communication inter-processus (IPC, Inter-Process Communication) qui fonctionne un peu comme un feu routier : vert on passe, orange on ralentit, rouge on ne passe pas. Le sémaphore doit bloquer le processus pChance tant que le processus pBonsoir n'aura pas fini sa tâche. Le sémaphore modélise en fait un mutex au niveau des threads mais le principe est le même.

Pour modéliser un sémaphore, on va utiliser une variable globale, sema, qui sera initialisée par un processus init qui s'occupera de l'initialisation du système, puis le sémaphore sera incrémenté ou décrémenté par les processus pChance et pBonsoir.

Pour le type de sema, on peut utiliser un byte, puisque sa valeur ne devrait pas dépasser le nombre de processus. Le langage Promela gère les types suivants :

Vous remarquerez qu'il n'y a ni nombres décimaux (float), ni pointeurs et cela est voulu par les concepteurs de Spin car il s'agit avant tout d'un langage de modélisation et non de programmation. Il sert uniquement àdécrire un modèle abstrait et non à développer un logiciel informatique. De plus un modèle doit rester simple et compréhensible pour éviter qu'on en vienne à modéliser le modèle. Cependant, le langage Promela intègre également les tableaux, les structures, les defines et les canaux de communication. [10]

Remarque importante : en Promela, il n'y a pas de différence entre une condition et une instruction, seul compte son exécutabilité ; soit l'instruction s'exécute, soit elle est bloquée, en attente d'exécution. [11]

Par exemple, une boucle while comme :

peut être remplacée par une condition :

Ainsi pour attendre que sema soit égale à zéro, on utilisera une condition sema == 0. Le processus pChance attendra que le sémaphore soit égale à un, tandis que pBonsoir incrémentera le sémaphore s'il est a zéro. Ainsi, l'affichage devrait apparaître dans l'ordre dans tout les cas, en principe.

On obtient le modèle suivant :

A priori, la simulation se déroule bien : le sémaphore force le processus pChance à se mettre en attente (le mode interactif ne l'affiche pas tant que pBonsoir n'a pas été lancé) et la phrase est affichée dans l'ordre. A présent, nous allons vérifier si ce modèle est valide, en passant sur le troisième onglet, l'onglet Verification.

2.1.3 …risque d'interblocage

En cliquant sur Run dans la partie Verification, Spin va générer, à partir du modèle Promela, un fichier pan.c (pan comme protocole analyzer, historiquement Spin fut développé pour l'analyse de protocoles). Ce fichier contient les instructions pour la validation. A son exécution, on peut lire en début de vérification l'erreur suivante :

Invalid end state est une erreur de type interblocage (deadlock). Cela signifie qu'un processus est en attente d'une ressource accaparée par un autre processus, mais cet autre processus est également en attente d'une ressource du processus pour libérer sa ressource. Les processus s'attendent donc mutuellement pour continuer leurs tâches : le système est bloqué. Un peu comme un quart-four où tout les feux seraient bizarrement au rouge et attendent que l'un passe au vert pour savoir combien de temps ils doivent rester au rouge. Il arrive ainsi que certaines applications multi-threads se figent par inadvertance, sans qu'il soit possible d'en reprendre le contrôle.

Spin peut vérifier, entre autre, les deadlock, les famines (livelock, accès à une ressource indisponible), les sous-spécifications (underspecifications, comme la non prise en charge d'un message), les sur-spécifications (overspecifications, surcharges qui génèrent du code mort) et les violations de contraintes (assertions).

Pour en revenir à notre exemple, celui-ci n'a qu'une seule ressource partagée, le sémaphore sema, source à priori de l'erreur. On a un processus init qui démarre en premier, puis les autres processus s'activent mais rien n'empêche le processus pBonsoir ou le processus pChance de démarrer avant que l'instruction d'affectation sema = 0 soit traitée.

La validation (verification) a généré un fichier .trail. Celui-ci va être réutilisé durant une nouvelle Simulation pour simuler le blocage et va nous permettre de trouver l'erreur. On revient donc sur l'onglet Simulate, on relance la simulation et là... c'est le drame. La simulation affiche :

En effet, la simulation, avec les résultats de validation, indique un cas d'exécution où le processus pBonsoir s'est lancé avant que l'initialisation de sema ait eu lieu. Du coup, pBonsoir incrémente sema, puis sema est initialisée à 0 par le processus init, et pChance, qui attend sema == 1,est bloqué.

2.1.4 Solution

Une solution est de démarrer les processus par le processus init, après l'initialisation du sémaphore. Pour ce faire, on fait appel à l'instruction run et l'on supprime les instructions active. On pourrait également supprimé le sémaphore, vu l'ordre séquentiel d'initialisation des processus, mais le temps d'exécution au sein d'un processus est indépendant des autres processus sans mécanismes de synchronisation.

On obtient donc le programme suivant :

La simulation se déroule comme prévue et la vérification ne détecte plus d'erreur. Le modèle est validé.

Ce simple exemple nous aura montré l'importance de l'initialisation dans les systèmes multi-processus ou multi-threads. Une variable qui n'aurait pas été initialisée à temps au moment où un thread démarre peut rendre le système incohérent. On aura vu également que ce cas n'arrive pas systématiquement : le model-checker aura parcouru les cas possibles d'exécution jusqu'à trouver celui qui génère une erreur.

2.2 The middle of the article

« First Fish: Morning.

Second Fish: Morning.

Third Fish: Morning.

Fourth Fish: Morning.

Third Fish: Morning.

First Fish: Morning.

Second Fish: Morning.

Fourth Fish: What's new?

First Fish: Not much.

Fifth and Sixth Fish: Morning. »

-- Monty Python : The Meaning of Life

2.3 Le protocole de salutation

Bien que l'on puisse utiliser Spin pour modéliser tout type de systèmes, Spin fut à l'origine conçu pour valider les protocoles de communication. Dans cet exemple, nous allons modéliser et valider un petit protocole de communication.

Les acteurs du système sont deux poissons d'un aquarium, Bob et Alice. Le protocole veut qu'à chaque fois qu'un poisson rencontre un nouveau poisson, il le salue. S'il l'a déjà salué et qu'ils se rencontrent à nouveau, le poisson doit lui demander de ses nouvelles. Bien entendu, un poisson ne doit pas saluer deux fois de suite le même poisson, ni lui redemander de ses nouvelles.   

2.3.1 Quand Bob rencontre Alice

Lorsque Bob rencontre Alice, il la salue et elle lui répond par le même salut. Autrement dit, Bob lui envoie un paquet SYN (demande de SYNchronisation) et elle lui renvoi un paquet ACK (accusé de réception, ACKnowledgement).

Pour modéliser cela, on utilise un processus générique pPoisson, avec un type de paquet mtype énumérant pour l'instant les paquets RST (Reset), SYN, ACK et FIN (Fin de transfert). mtype est un méta-type unique qui sert à modéliser toutes les énumérations du système.

On aura également besoin d'un canal de communication, comme une socket TCP, un tube, une file de message ou, en l'occurrence, des ondes sonores en milieu aquatique que l'on modélise par un chan message (chan message = [N] of {mtype}, où N est la taille du buffer, si N = 0, les messages ne font que transiter).

On obtient un premier programme suivant :

On a d'abord définit les énumérations des protagonistes et des paquets (mtype), ainsi que le canal de messages (chan) qui transfert des paquets de type mtype.

Ensuite, on définit le processus pPoisson. Celui-ci contient deux sauts conditionnels if qui se terminent par des fi. Attention toutefois à ne pas confondre avec l'instruction if du C et du C++ : ici, Spin se met en attente que l'une des conditions commençant par des doubles points (::)soit satisfaite, un peu comme un switchbloquant.

Ce modèle commence par réveiller les deux poissons Bob et Alice (run pPoisson(bob); run pPoisson(alice)), lesquels se mettent en attente d'un paquet RST ou SYN dans la première instruction if.

Ensuite le modèle envoie un paquet RST (ligne 21 : message!RST). Celui-ci est capturé par le premier poisson, en l'occurrence Bob, qui salut (printf avec un  %e pour un mtype) et envoie un paquet SYN (ligne 8 : message!SYN). Bob se met ensuite en attente d'un paquet ACK ou FIN (second if).

Le paquet SYN envoyé par Bob est récupéré par Alice (ligne 9 : message?SYN), qui répond et envoi un accusé de réception ACK (ligne 9 : message!ACK). Puis Alice se met également en attente d'un paquet ACK ou FIN (second if).

Bob récupère le paquet ACK (ligne 12) et envoie un paquet FIN, lequel est reçut par Alice (ligne 13).

En effectuant la simulation, vous pourrez également observer un magnifique graphique correspondant à cet échange protocolaire. Ce modèle passe également la validation.

2.3.2 Sinon, quoi de neuf ?

Cette fois, nos deux protagonistes parviennent à l'autre bord de l'aquarium, ils se retournent et se rencontrent de nouveau. Au lieu de se saluer, le premier demande des nouvelles du second. Pour ce faire, on va ré-émettre un paquet reset et utiliser une variable partagée new_rst (pour nouveau paquet RST) qu'on aura bien initialisée avant le démarrage des processus pPoisson. On utilise également la notation -> (un séparateur d'instructions comme ;) pour plus de clarté. Le modèle précédent ne devrait pas trop être modifié. On aurait bien aimé simplifier avec quelques opérateurs&& mais ce n'est pas possible, à priori, avec un canal chan en opérande. On ajoute également une boucle do, pour le nouveau reset, qui se répète jusqu'à trouver une instruction break.

On obtient le modèle suivant :

Ce modèle affiche :

Ce modèle est valide et correspond bien à notre protocole, avec deux communications complètes, bien visible sur le graphe protocolaire de simulation.

Conclusion

Les model-checkers sont des outils essentiels de modélisation et de validation de systèmes. Par la vérification de tout les cas possibles, ils offrent une validation à posteriori, qui se rapproche des cas non-prévus que l'on peut rencontrer par inadvertance dans la réalité, comme un débordement de tampon, une variable non initialisée, une attente infinie de message, cas difficilement détectable par d'autres outils car ce sont des erreurs qui n'apparaissent pas systématiquement, non-reproductibles. Les validations de modèles peuvent s'effectuer en parallèle de la conception et du développement logiciel classique.

Avec Spin et son interface iSpin, on aura réalisé et validé quelques modèles en Promela, en particulier des modèles de protocoles et de systèmes multi-processus (ou multi-threads). Aussi Spin peut être très utile, voire indispensable, pour valider les systèmes faisant intervenir des communications inter-processus complexes.

On aura également vu quelques instructions de bases du langage Promela et utilisé Spin de façon ludique, mais Spin possède également bien d'autres fonctions d'utilisation, de vérification et de validation que l'on n'aura pas abordé dans cet article, comme le support direct pour les systèmes embarqués en langage C.

Spin est aujourd'hui toujours activement maintenu par le laboratoire Bell et le JPL/Caltech (Jet Propulsion Laboratory – Nasa), il est régulièrement mis-à-jour et possède quelques extensions ainsi qu'un site web bien documenté sur lequel on peut trouver bon nombre d'exemples et de tutoriels.

Et bonne chance, bonsoir [invalid end state].

Références

[1] L.M.G. FEIJS, H.B.M. JONKERS, Formal Specification and Design, Cambridge University Press, 1992.

[2] J.M. SCHUMANN, Automated Theorem Proving in Software Engineering, Springer, 2001.

[3] M. BEN-ARI, Principles of the Spin Model Checker, Springer, 2008.

[4] CLEARSY, Atelier B, http://www.atelierb.eu, 2013.

[5]UNIVERSITYOF CAMBRIDGE, Isabelle, http://isabelle.in.tum.de, 2013.

[6] P. BAUDIN, F. BOBOT, R. BONICHON et al. Frama-C, http://frama-c.com, 2013.

[7] UNIVERSITY OF TEXAS AT AUSTIN, ACL2, http://www.cs.utexas.edu/users/moore/acl2/, 2013.

[8] ALCATEL LUCENT, Bell Labs, http://www3.alcatel-lucent.com/wps/portal/belllabs, 2013.

[9] SPINROOT, Spin Precompiled Executables,http://spinroot.com/spin/Bin/index.html, 2013.

[10] SPINROOT, Promela data types, http://spinroot.com/spin/Man/datatypes.html, 2013.

[11] SPINROOT, Manual, http://spinroot.com/spin/Man/Manual.html, 2013.