Proving Systolic Systems Correct

Abstract

A language for describing communicating systems is described. It is sufficiently expressive to describe both the desired behavior of systems, their specifications, and their actual implementations in terms of simpler components. We say I satisfies S if 1 is a correct implementation of the specification S. We briefly discuss a semantic treatment of this notion of satisfaction, but the main emphasis of the paper is on a proof technique for proving statements of the form I satisfies S, based on syntactic transformations and induction. Two examples are given, both systolic systems from the literature. © 1986, ACM. All rights reserved.