Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi M., Lamport L. (1991): The Existence of Refinement Mappings. In: Journal of TCS 1991, Volume 82, number 2, pages 253–284
Abadi M., Lamport L. (1995): Conjoining Specifications. TOPLAS (3), Pages 507–534, Volume 17
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.
Lamport L. (1994): The Temporal Logic of Actions. In: Journal of ACM Transactions on Programming Languages and Systems, number 3, Volume 16
Lamport L. (1996): The Syntax and Semantics of TLA+. Partl: Definitions and Modules Report: http://www.research.digital.com/SRC/tla/
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.
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–530
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.
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 315
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.
Zohar Manna and Amir Pnueli (1991): The Temporal Logic of Reactive and Concurrent Systems Springer, 1991.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Wien
About this paper
Cite this paper
Rock, G., Stephan, W., Wolpers, A. (1999). Modular reasoning about structured TLA specifications. In: Berghammer, R., Lakhnech, Y. (eds) Tool Support for System Specification, Development and Verification. Advances in Computing Science. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6355-9_16
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6355-9_16
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-83282-0
Online ISBN: 978-3-7091-6355-9
eBook Packages: Springer Book Archive