Interface refinement in reactive systems

Abstract

Suppose one has a system that has a synchronous interface with its environment. Now, suppose that one refines this system and changes its interface to an asynchronous one. Whatever is meant here by refinement, it cannot be standard (process) refinement since the interface actions have changed; nor is it action refinement in the sense that a process is substituted for an action, as the intention presumably is to allow the system to proceed without having to wait until the environment is willing to synchronize. In this paper we propose a notion of interface refinement of which changing synchronous to asynchronous communication is an instance; as is in fact the reverse change. This notion of interface refinement is quite powerful; it generalizes all existing methods w.r.t, the class of interface changes that it allows. The major part of the paper is concerned with developing proof rules with which to verify interface refinement. We use (finear) temporal logic as specification language and an adaptation of the Manna-Pnueli verification framework. The method is illustrated by verifying an interface change in which synchronous communication is replaced by asynchronous send and receive. Proofs of the various theorems and lemma’s are delegated to an appendix.