Towards a Formal Treatment of Implicit Invocation Using Rely/Guarantee Reasoning
- 1 March 1998
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 10 (3) , 193-213
- https://doi.org/10.1007/s001650050011
Abstract
: Implicit invocation [SuN92, GaN91] has become an important architectural style for large-scale system design and evolution. This paper addresses the lack of specification and verification formalisms for such systems. A formal computational model for implicit invocation is presented. We develop a verification framework for implicit invocation that is based on Jones' rely/guarantee reasoning for concurrent systems [Jon83, Stø91]. The application of the framework is illustrated with several examples. The merits and limitations of the rely/guarantee paradigm in the context of implicit invocation systems are also discussed.Keywords
This publication has 7 references indexed in Scilit:
- A framework for event-based software integrationACM Transactions on Software Engineering and Methodology, 1996
- Reconciling environment integration and software evolutionACM Transactions on Software Engineering and Methodology, 1992
- Formalizing design spaces: Implicit invocation mechanismsPublished by Springer Nature ,1991
- A method for the development of totally correct shared-state parallel programsPublished by Springer Nature ,1991
- Tentative steps toward a development method for interfering programsACM Transactions on Programming Languages and Systems, 1983
- A Calculus of Communicating SystemsLecture Notes in Computer Science, 1980
- An axiomatic proof technique for parallel programs IActa Informatica, 1976