A High-Level Language for Modeling Algorithms and their Properties

Sabina Akhtar 1 Stephan Merz 1 Martin Quinson 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 ALGORILLE - Algorithms for the Grid
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Designers of concurrent and distributed algorithms usually express them using pseudo-code. In contrast, most verification techniques are based on more mathematically-oriented formalisms such as state transition systems. This conceptual gap contributes to hinder the use of formal verification techniques. Leslie Lamport introduced PlusCal, a high-level algorithmic language that has the "look and feel" of pseudo-code, but is equipped with a precise semantics and includes a high-level expression language based on set theory. PlusCal models can be compiled to TLA+ and verified using the model checker tlc. However, in practice the use of PlusCal requires good knowledge of TLA+ and of the translation from PlusCal to TLA+ . In particular, the user needs to annotate the generated TLA+ model in order to define the properties to be verified and to introduce fairness hypotheses. Moreover, the PlusCal language enforces certain restrictions that often make it difficult to express distributed algorithms in a natural way. We propose a new version of PlusCal with the aim of overcoming these limitations, and of providing a language in which algorithms and their properties can be expressed naturally. We have implemented a compiler of our language to TLA+ , supporting the verification of algorithms by finite-state model checking.
Type de document :
Communication dans un congrès
13th Brazilian Symposium on Formal Methods - SBMF'2010, Nov 2010, Natal, Brazil. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00537779
Contributeur : Martin Quinson <>
Soumis le : vendredi 19 novembre 2010 - 12:11:30
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 16:01:03

Identifiants

  • HAL Id : inria-00537779, version 1

Collections

Citation

Sabina Akhtar, Stephan Merz, Martin Quinson. A High-Level Language for Modeling Algorithms and their Properties. 13th Brazilian Symposium on Formal Methods - SBMF'2010, Nov 2010, Natal, Brazil. 2010. 〈inria-00537779〉

Partager

Métriques

Consultations de la notice

265

Téléchargements de fichiers

422