A User's Guide to TLA

Stephan Merz
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 
  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}

Stephan Merz
Last modified: Sun Feb 16 12:17:05 MET 2003