Proving systolic systems correct
Author:
Open Access
- 1 June 1986
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 8 (3) , 344-387
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.Keywords
This publication has 9 references indexed in Scilit:
- Systolic VLSI Arrays for Polynomial GCD ComputationIEEE Transactions on Computers, 1984
- Testing equivalences for processesTheoretical Computer Science, 1984
- Synchronous and asynchronous experiments on processesInformation and Control, 1983
- Calculi for synchrony and asynchronyTheoretical Computer Science, 1983
- Optimizing synchronous systems1981
- A Calculus of Communicating Systems1980
- Flowgraphs and Flow AlgebrasJournal of the ACM, 1979
- A system which automatically improves programsActa Informatica, 1976
- Real-Time Computation by n-Dimensional Iterative Arrays of Finite-State MachinesIEEE Transactions on Computers, 1969