SPIN model checker

Pour les articles homonymes, voir Spin (homonymie).

SPIN model checker

Informations

Développé par	Gerard Holzmann
Première version	1989[1]
Dernière version	6.5.2 (6 décembre 2019)[2]
Dépôt	github.com/nimble-code/Spin
Écrit en	C
Système d'exploitation	Linux, Microsoft Windows et macOS
Type	Model checking
Licence	BSD 3-clauses
Site web	spinroot.com

modifier - modifier le code - voir Wikidata (aide)

SPIN est un outil général pour vérifier la correction de modèles logiciels concurrents de manière rigoureuse et généralement automatisée. Il a été écrit, à partir de 1980, par Gerard J. Holzmann et d'autres membres du groupe Unix du Computing Sciences Research Center des Bell Labs. Le logiciel est disponible gratuitement depuis 1991 et continue d'évoluer pour suivre le rythme des nouveaux développements dans ce domaine.

Les systèmes à vérifier sont décrits en langage Promela (abréviation pour Process Meta Language), langage qui supporte la modélisation des algorithmes distribués asynchrones, décrits en tant qu'automates non déterministes (SPIN signifie « Simple Promela Interpreter »). Les propriétés à vérifier sont exprimées sous forme de formules de logique temporelle linéaire (LTL), qui sont niées puis converties en automates de Büchi. En plus de sa fonction de vérificateur de modèles, SPIN peut également opérer comme simulateur, en suivant l'un chemin d'exécution possible à travers le système et en présentant la trace d'exécution résultante à l'utilisateur.

Contrairement à de nombreux vérificateurs de modèles, SPIN n'effectue pas lui-même la vérification de modèles, mais génère à la place des sources C pour un vérificateur de modèles spécifique adapté au problème. Cette technique économise de la mémoire et améliore les performances, tout en permettant également l'insertion directe de morceaux de code C dans le modèle. SPIN propose également un grand nombre d'options pour accélérer davantage le processus de vérification et économiser de la mémoire, telles que:

• réduction par ordre partiel ;
• compression d'états;
• hachage d'états par bits (en) (au lieu de stocker des états entiers, seul leur hash code est mémorisé dans un champ de bits; cela économise beaucoup de mémoire mais aux dépens de l'exhaustivité) ;
• faible exigence sur l'équité.

Depuis 1995 environ, des ateliers SPIN annuels ont été organisés pour les utilisateurs SPIN, les chercheurs et les personnes généralement intéressées par la vérification de modèles . Le 26^e workshop a eu lieu en 2019 à Pékin^[3].

En 2001, l'Association for Computing Machinery a décerné à SPIN son Prix ACM Software System^[4].

• NuSMV
• Uppaal Model Checker (en)

• Gerard J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2004, 598 p. (ISBN 0-321-22862-6, lire en ligne).
• Samuel Hym, « SVL ― Introduction au Model-Checker Spin », Université de Lille, département informatique de la Faculté des Sciences et Technologies, 2008 (consulté le 22 septembre 2020).
• Balima Damien, « Spin model checker », Open Silicium, Open Silicium, n^o 9,‎ décembre 2013 (lire en ligne, consulté le 22 septembre 2020).

• Site Web SPIN

• Portail de l’informatique