Publication
Modular Reasoning about Structured TLA Specifications
Georg Rock; Werner Stephan; Andreas Wolpers
In: R. Berghammer; Y. Lakhnech (Hrsg.). 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.
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.