LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Cubicle est un model-checker pour vérifier des propriétés de sureté d'algorithmes faisant intervenir un nombre quelconque de processus. Ces algorithmes sont d écrits sous forme de systèmes de transitions dits paramètres. Les propriétés de sureté ainsi que les états du système sont décrits par des formules logiques du premier ordre. Pour vérifier ces propriétés, Cubicle met en oeuvre un algorithme d'atteignabilité par chaînage arrière qui utilise un démonstrateur SMT (Satisabilité Modulo Théories). Les expériences, menées sur la vérification d'algorithmes d'exclusion mutuelle et de protocoles de cohérence de cache, montrent que Cubicle est efficace et compétitif avec les model checkers de la même famille. Cubicle est un logiciel libre d éveloppé en OCaml. Il utilise le démonstrateur Alt-Ergo zero, une version allégée et améliorée d'Alt-Ergo. Une implantation parallèle se reposant sur la bibliothèque Functory est également proposée.
https://hal.inria.fr/hal-00778832
Contributeur : Ist Inria Saclay
<>
Soumis le : lundi 21 janvier 2013 - 14:56:42
Dernière modification le : vendredi 6 avril 2018 - 14:34:04
Document(s) archivé(s) le : samedi 1 avril 2017 - 07:46:42
Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs - 2013, Feb 2013, Aussois, France. 2013. 〈hal-00778832〉
