A High-Level Language for Modeling Algorithms and Their Properties - Formal Methods: Foundations and Applications - page 49

A High-Level Language for Modeling Algorithms
and Their Properties

Sabina Akhtar, Stephan Merz, and Martin Quinson

LORIA - INRIA Nancy Grand Est and Nancy University, Nancy, France
{ Sabina.Akhtar,Stephan.Merz,Martin.Quinson } @loria.fr

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 com-
piled 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
dicult to express distributed algorithms in a natural way. We propose
anewversionofPlusCal 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.

1 Introduction

Algorithms for concurrent and distributed systems [11] are notoriously hard to
design, due to the number of interleavings of their constituent processes that
must communicate and synchronize properly in order to achieve the desired
function. It is all too easy to overlook corner cases, and hard to generate or
reproduce particular behaviors during testing. Formal verification of such algo-
rithms is therefore essential, and model checking in particular has been applied
with great success in this context. However, there is a conceptual gap between the
languages algorithm designers use to convey their ideas and the input languages
of model checking tools. While the former emphasize high levels of abstraction
in order to present the algorithmic ideas, their semantics is not precisely defined.
Languages for model checkers come with a more precise (at least operational)
semantics but tend to make compromises in terms of the available data types
in order to enable compact state representations and the ecient computation