Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm

Publisher Website
Google Scholar
Abstract
This paper presents an assumption/commitment specification technique and a refinement calculus for networks of agents communicating asynchronously via unbounded FIFO channels in the tradition of Kahn. We define two types of assumption/commitment specifications, namely simple and general specifications. It is shown that semantically, any deterministic agent can be uniquely characterized by a simple specification, and any nondeterministic agent can be uniquely characterized by a general specification. We define two sets of refinement rules, one for simple specifications and one for general specifications. The rules are Hoare-logic inspired. In particular the feedback rules employ invariants in the style of a traditional while-rule. Both sets of rules have been proved to be sound and also (semantic) relative complete. Conversion rules allow the two logics to be combined. This means that general specifications and the rules for general specifications have to be introduced only at the point in a system development where they are really needed.

This publication has 21 references indexed in Scilit: