TLA + PROMELA: Conjecture, check, proof

Engineering new protocols using methods and formal notations
  • J. -Ch. Grégoire
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


Refinement is the best established method to verify complex models using proof-theoretic techniques. One of the challenge of applying this method, besides the tediousness of the proofs, is the slow feedback in assessing the adequacy of the models. In this paper, we show how the tool SPIN has been used to help with formal proofs of a hierarchy of models specified in TLA+. Without being a substitute for a formal proof, using SPIN in this context can reduce the workload by providing a means to quickly assess models, invariants and refinement mappings.


TLA+ TLA SPIN PROMELA refinement implementation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Martin Abadi and Stephan Merz. On TLA as a logic. In Manfred Broy, editor, Deductive Program Design, pages 235–271. NATO ASI Series, Springer-Verlag, 1995.Google Scholar
  2. 2.
    J.-R. Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
  3. 3.
    J. Hajek. Automatically verified data transfer protocols. In 4th ICCC pages 749–756, 1978.Google Scholar
  4. 4.
    Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME '96, number 1051 in Lecture Notes in Computer Science, pages 662–681, Oxford, UK, March 1996. Springer-Verlag.Google Scholar
  5. 5.
    P. Herrmann and H. Krumm. Re-usable verification elements for high-speed transfer protocol configu ration. In Protocol Specification, Testing and Verification XV, pages 171–186. Chapman & Hall, 1995.Google Scholar
  6. 6.
    Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.Google Scholar
  7. 7.
    Gerard J. Holzmann and Doron Peled. An improvement in formal verification. In Dieter Hogrefe and Stefan Leue, editors, 7th Int. Conf. on Formal Description Techniques. Chapman and Hall, 1994.Google Scholar
  8. 8.
    Peter Ladkin. Formal but lively buffers in TLA+. Technical report, Universität von Bielefeld, 1996. from Scholar
  9. 9.
    Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872–923, 1994.Google Scholar
  10. 10.
    Leslie Lamport. TLA+. Technical report, DEC-SRC, 1995. from Scholar
  11. 11.
    Zoar Manna and Amir Pnueli. A Temporal Proof Methodology for Reactive Systems. In Program Design Calculi, NATO ASI Series, Series F. Springer Verlag, 1993.Google Scholar
  12. 12.
    Natarajan and G.J. Holzmann. Towards a formal semantics of PROMELA. In Proceedings of the 2nd SPIN Workshop, 1996.Google Scholar
  13. 13.
    S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification of fault-tolerant architectures: Prolegmena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • J. -Ch. Grégoire
    • 1
  1. 1.INKS-TélécommunicationsFrance

Personalised recommendations