Modular Reasoning about Structured TLA Specifications

Georg Rock, Werner Stephan, Andreas Wolpers

In: R. Berghammer , Y. Lakhnech (editor). Tool Support for System Specification, Development and Verification. International Workshop Tool Support for System Specification, Development and Verification Pages 217-229 Advances in Computing Science Springer 1999.


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.

Weitere Links

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz