A High-Level Language for Modeling Algorithms and Their Properties

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 pseudocode, 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 distribute...

• Type: Journal
• Year: 2010
• Where: SBMF
• Authors: Sabina Akhtar, Stephan Merz, Martin Quinson
• Keywords: Algorithms, Formal Methods, Formal Verification Techniques, SBMF 2010, Verification Techniques