Interface refinement in reactive systems (extended abstract)

R.T. Gerth, R. Kuiper, J.P.L. Segers

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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 (linear) 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.
Original languageEnglish
Title of host publicationCONCUR'92 (Proceedings 3rd International Conference on Concurrency Theory, Stony Brook NY, USA, August 24-27, 1992)
EditorsR. Cleaveland
Place of PublicationBerlin
PublisherSpringer
Pages77-93
ISBN (Print)3-540-55822-5
DOIs
Publication statusPublished - 1992

Publication series

NameLecture Notes in Computer Science
Volume630
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Interface refinement in reactive systems (extended abstract)'. Together they form a unique fingerprint.

Cite this