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

LOTOS [1] (Language of Temporal Ordering Specifications) is a formalism
for specifying distributed systems, specifically related to Open Systems Inter-
connection (OSI) computer network architecture. Estelle [2] is another formal
description technique for writing specification for concurrent and distributed
information processing systems. It is based on Extended State Transistion sys-
tems and is supported by industrial-strength tools. Both languages are similar
in purpose to Promela, whereas we are aiming at obtaining higher-level de-
scriptions of algorithms, for which abstract data representations in terms of sets
and functions are more useful.
There exist many other languages that are closer to the programming languages
rather than formal specification languages. They serve as inputs to verification
tools and/or for generating executable code. For example, Mace [5] is a language
for building distributed systems. It is a C++ language extension that translates
distributed system specifications into a C++ implementation. Model checking can
be performed at a higher level using the MaceMC model checker. In contrast,
PlusCal is intended as a language that algorithm designers use to communicate
(and validate) their ideas, not for generating ecient implementations.
6Conluon
PlusCal is a high-level language that aims at natural expression of algorithms;
it makes formal verification easily accessible to algorithm designers. We have
identified certain limitations of the original language and have defined a new
version that tries to overcome them. In particular, we have strived at making
algorithm descriptions entirely self-contained, so that knowledge of TLA + ,and
in particular of the PlusCal compiler, is no longer a prerequisite for using
PlusCal. We have also made the language more uniform, removing some lim-
itations and adding features such as nested processes, scoped declarations, and
user-defined grain of atomicity. We believe that the new version significantly
simplifies the representation of algorithms in PlusCal andthatitwillbemore
accessible to users who are not experts in formal methods.
In future work, we are planning to address reduction techniques for mitigating
the effect of state space explosion. In particular, we plan to implement partial-
order reduction for verifying models written in PlusCal. In concurrent and
distributed systems, the execution of independent events in an arbitrary order
results in the same overall system state, and it is therefore enough to consider
only one interleaving of such events. Eciently verifying that two events are
independent is, however, non-trivial, and adding locality to PlusCal was an
important first step in identifying sucient conditions for two statements being
independent.
On a more technical level, it would be beneficial to translate counter-examples
produced by tlc back to the level of PlusCal programs in order to make them
easier to understand for PlusCal users. We also plan to integrate our PlusCal
language into the TLA + toolbox that has recently been released. 5
5 http://www.tlaplus.net/