Towards a Formal Treatment of Implicit Invocation Using Rely/Guarantee Reasoning
Towards a Formal Treatment of Implicit Invocation Using Rely/Guarantee Reasoning
复制标题
使用依赖/保证推理对隐式调用进行正式处理
DOI：
--
复制
发表时间：
1997
影响因子：
1
通讯作者：
D. Notkin
中科院分区：
文献类型：
--
作者：
Jürgen Dingel;D. Garlan;S. Jha;D. Notkin
抽象。隐式调用[SuN 92，GaN 91]已经成为大规模系统设计和演化的重要架构风格。本文讨论了缺乏规范和验证形式主义，这样的系统。提出了一种隐式调用的形式化计算模型。我们开发了一个隐式调用的验证框架，该框架基于Jones的并发系统的依赖/保证推理[Jon 83，Stø 91]。该框架的应用说明了几个例子。本文还讨论了隐式调用系统中依赖/保证范式的优点和局限性。
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.