Process simulation and refinement

He Jifeng

doi:10.1007/BF01887207

Process simulation and refinement

He Jifeng^*

^*此作品的通讯作者

University of Oxford

科研成果: 期刊稿件 › 文章 › 同行评审

37 引用（Scopus）

摘要

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.

源语言	英语
页（从-至）	229-241
页数	13
期刊	Formal Aspects of Computing
卷	1
期	1
DOI	https://doi.org/10.1007/BF01887207
出版状态	已出版 - 3月 1989
已对外发布	是

访问文件

10.1007/BF01887207

其它文件与链接

链接到 Scopus 的出版物

引用此

@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

摘要

访问文件

其它文件与链接

指纹

引用此