A User's Guide to TLA

Stephan Merz

Contents

This paper is an elaboration of a talk given at a summer school on the modeling and verification of parallel processes in Nantes (1998). It attempts to present the main concepts of Lamport's TLA and its use for system specification, including styles of specification and elementary verification rules.

Available as:  gzip'ed Postscript 

Reference

@InProceedings{merz:userguide,
  author =    {Stephan Merz},
  title =     {A User's Guide to {TLA}},
  booktitle = {Mod{\'e}lisation et v{\'e}rification des processus
               parall{\`e}les: Actes de l'{\'e}cole d'{\'e}t{\'e}},
  editor =    {F. Cassez and C. Jard and O. Roux and B. Rozoy},
  year =      1998,
  publisher = {Ecole centrale de Nantes},
  address =   {Nantes, France},
  month =     jul,
  pages =     {29--44}
}