Process simulation and refinement
- 1 March 1989
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 1 (1) , 229-241
- https://doi.org/10.1007/bf01887207
Abstract
In this paper we deal with the problem of (nondeterministic and parallel) process refinement. The basic notion of refinement is defined via the improved failure semantics of CSP [BHR84, BrR85, Hoa85, Ros88]. The concept of simulation of Communicating Systems introduced in [Mil80, Par81] is generalised and proved to be sound for the correctness of refinement. A Galois connection is presented to show that up-simulation and down-simulation together provide a complete proof method. The paper also suggests that simulation can be employed to derive an implementation from a specification.Keywords
This publication has 6 references indexed in Scilit:
- Concurrency and automata on infinite sequencesPublished by Springer Nature ,2005
- The weakest prespecificationInformation Processing Letters, 1987
- An improved failures model for communicating processesPublished by Springer Nature ,1985
- A Theory of Communicating Sequential ProcessesJournal of the ACM, 1984
- A Calculus of Communicating SystemsLecture Notes in Computer Science, 1980
- Beiträge zur Filtertheorie. IIMathematische Nachrichten, 1953