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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks 14 (1987)
Budkowski, S., Dembinski, P.: An introduction to Estelle: A specification language for distributed systems. Comput. Netw. ISDN Syst. 14(1), 3–23 (1987)
Dijkstra, E.W.: Guarded commands, non-determinacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)
Killian, C.E., Anderson, J.W., Braud, R., Jhala, R., Vahdat, A.: Mace: Language Support for Building Distributed Systems. In: PLDI, pp. 179–188 (2007)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Lamport, L.: A fast mutual-exclusion algorithm. ACM Trans. Computer Systems 5(1), 1–11 (1987)
Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2002)
Lamport, L.: Checking a multithreaded algorithm with +CAL. In: Dolev, S. (ed.) DISC 2006. LNCS, vol. 4167, pp. 151–163. Springer, Heidelberg (2006)
Lamport, L.: A +CAL user’s manual (2007), http://research.microsoft.com/en-us/um/people/lamport/tla/pluscal.html
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Naimi, M., Trehel, M., Arnold, A.: A log(n) distributed mutual exclusion algorithm based on path reversal. J. Parallel Distrib. Comput. 34(1), 1–13 (1996)
Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)
Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Akhtar, S., Merz, S., Quinson, M. (2011). A High-Level Language for Modeling Algorithms and Their Properties. In: Davies, J., Silva, L., Simao, A. (eds) Formal Methods: Foundations and Applications. SBMF 2010. Lecture Notes in Computer Science, vol 6527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19829-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-19829-8_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19828-1
Online ISBN: 978-3-642-19829-8
eBook Packages: Computer ScienceComputer Science (R0)