Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms

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 : The design of correct concurrent and distributed algorithms is notoriously difficult, and they are prone to errors such as deadlocks and race conditions. Model checking is one of the most successful formal techniques that are used to verify these algorithms. For example, TLC accepts models written in TLA+, a specification language based on mathematical set theory and the Temporal Logic of Actions. Such languages have a very different flavor from the (pseudo-)programming languages that algorithm designers typically use to express algorithms. PLUSCAL introduced by Leslie Lamport, is a high-level language for describing concurrent and distributed algorithms, from which TLA+ models are generated and then analyzed using TLC. Unfortunately, PLUSCAL suffers from a number of limitations that restricts its usefulness as an abstraction layer for the underlying TLA+ formalism.
Type de document :
Communication dans un congrès
Eric Cariou, Laurence Duchien, Yves Ledru. Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, Mar 2010, Pau, France. 2010
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00544137
Contributeur : Sabina Akhtar <>
Soumis le : mardi 7 décembre 2010 - 14:49:41
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : mardi 8 mars 2011 - 04:16:36

Fichier

GDR-GDL_Sabina.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00544137, version 1

Collections

Citation

Sabina Akhtar, Stephan Merz, Martin Quinson. Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms. Eric Cariou, Laurence Duchien, Yves Ledru. Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, Mar 2010, Pau, France. 2010. 〈inria-00544137〉

Partager

Métriques

Consultations de la notice

345

Téléchargements de fichiers

142