Vérification de systèmes paramétrés avec Cubicle

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-00778832
Contributor : Ist Inria Saclay <>
Submitted on : Monday, January 21, 2013 - 2:56:42 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Saturday, April 1, 2017 - 7:46:42 AM

File

jfla2013-02.pdf
Explicit agreement for this submission

Identifiers

  • HAL Id : hal-00778832, version 1

Collections

Citation

Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France. ⟨hal-00778832⟩

Share

Metrics

Record views

477

Files downloads

418