SPIN model checker

Un article de Wikipédia, l'encyclopédie libre.
SPIN model checker

Informations
Développé par Gerard HolzmannVoir et modifier les données sur Wikidata
Première version [1]Voir et modifier les données sur Wikidata
Dernière version 6.5.2 ()[2]Voir et modifier les données sur Wikidata
Dépôt github.com/nimble-code/SpinVoir et modifier les données sur Wikidata
Écrit en CVoir et modifier les données sur Wikidata
Système d'exploitation Linux, Microsoft Windows et macOSVoir et modifier les données sur Wikidata
Type Model checkingVoir et modifier les données sur Wikidata
Licence BSD 3-clausesVoir et modifier les données sur Wikidata
Site web spinroot.comVoir et modifier les données sur Wikidata

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.

Description[modifier | modifier le code]

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:

Historique[modifier | modifier le code]

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 26e 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].

Voir aussi[modifier | modifier le code]

Références[modifier | modifier le code]

Documentation[modifier | modifier le code]

Liens externes[modifier | modifier le code]