Modular reasoning about structured TLA specifications

  • Georg Rock
  • Werner Stephan
  • Andreas Wolpers
Part of the Advances in Computing Science book series (ACS)


In this paper we propose a modular approach to the specification and verification of reactive and concurrent systems. An assumption-commitment style of specification is necessary in this context since no system will behave as expected if the environment does not fulfill the assumptions. However, assumption-commitment specifications can be circular in nature (Abadi Merz 1995) and so we are faced with the problem to rule out unsound circular reasoning.


Temporal Logic Combine System Proof Obligation Concurrent System State Predicate 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Abadi M., Lamport L. (1991): The Existence of Refinement Mappings. In: Journal of TCS 1991, Volume 82, number 2, pages 253–284MathSciNetMATHCrossRefGoogle Scholar
  2. Abadi M., Lamport L. (1995): Conjoining Specifications. TOPLAS (3), Pages 507–534, Volume 17CrossRefGoogle Scholar
  3. Abadi M., Merz S. (1995): An abstract account of composition. In: Proceedings MFCS 1995, Lecture Notes in Computer Science, volume 969, pages 499–508. Springer-Verlag, Berlin.Google Scholar
  4. Lamport L. (1994): The Temporal Logic of Actions. In: Journal of ACM Transactions on Programming Languages and Systems, number 3, Volume 16Google Scholar
  5. Lamport L. (1996): The Syntax and Semantics of TLA+. Partl: Definitions and Modules Report: Google Scholar
  6. Dieter Hutter, Bruno Langenstein, Claus Sengler, Jörg H. Siekmann, Werner Stephan and Andreas Wolpers (1996): Deduction in the Verification Support Environment (VSE). In: Proceedings Formal Methods Europe 1996: Industrial Benefits and Advances in Formal Methods Editor: Marie-Claude Gaudel and James Woodcock, SPRINGER.Google Scholar
  7. Dieter Hutter, Bruno Langenstein, Claus Sengler, Jörg H. Siekmann, Werner Stephan and Andreas Wolpers (1996): Verification Support Environment (VSE). In: Journal of High Integrity Systems 1996, volume 1, number 6, pages 523–530Google Scholar
  8. Dieter Hutter and Heiko Mantel and Georg Rock and Werner Stephan and Andreas Wolpers and Michael Balser and Wolfgang Reif and Gerhard Schellhorn and Kurt Stenzel (1998): VSE: Controlling the Complexity in Formal Software Development (1998): In: Current Trends in Applied Formal Methods (1998), to appear.Google Scholar
  9. Georg Rock, Werner Stephan, Andreas Wolpers (1997) Tool Support for the Compositional Development of Distributed Systems (1997): In: Tagungsband 7. GI/ITGFachgespräch Formale Beschreibungstechniken für verteilte Systeme. GMD Studien, number 315Google Scholar
  10. Stark, E.W. (1985): A proof technique for rely/guarantee properties. In: Foundations of Software Technology and Theoretical Computer Science, S.N. Maheshwari, Ed. Lecture Notes of Computer Science, volume 206, pages 369–391. Springer-Verlag.CrossRefGoogle Scholar
  11. Zohar Manna and Amir Pnueli (1991): The Temporal Logic of Reactive and Concurrent Systems Springer, 1991.Google Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • Georg Rock
  • Werner Stephan
  • Andreas Wolpers

There are no affiliations available

Personalised recommendations