Process simulation and refinement

He Jifeng

doi:10.1007/BF01887207

Process simulation and refinement

He Jifeng^*

^*Corresponding author for this work

University of Oxford

Research output: Contribution to journal › Article › peer-review

37 Scopus citations

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.

Original language	English
Pages (from-to)	229-241
Number of pages	13
Journal	Formal Aspects of Computing
Volume	1
Issue number	1
DOIs	https://doi.org/10.1007/BF01887207
State	Published - Mar 1989
Externally published	Yes

Keywords

Refinement
Simulation

Access to Document

10.1007/BF01887207

Cite this

@article{0fd77da600444120a7361a3a41558b96,

title = "Process simulation and refinement",

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 = "Refinement, Simulation",

author = "He Jifeng",

year = "1989",

month = mar,

doi = "10.1007/BF01887207",

language = "英语",

volume = "1",

pages = "229--241",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery (ACM)",

number = "1",

}

TY - JOUR

T1 - Process simulation and refinement

AU - Jifeng, He

PY - 1989/3

Y1 - 1989/3

N2 - 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.

AB - 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.

KW - Refinement

KW - Simulation

UR - https://www.scopus.com/pages/publications/34249970761

U2 - 10.1007/BF01887207

DO - 10.1007/BF01887207

M3 - 文章

AN - SCOPUS:34249970761

SN - 0934-5043

VL - 1

SP - 229

EP - 241

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 1

ER -

Process simulation and refinement

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this