A singleton failures semantics for Communicating Sequential Processes
A singleton failures semantics for Communicating Sequential Processes
复制标题
用于通信顺序进程的单例故障语义
DOI：
10.1007/s00165-005-0081-x
复制
发表时间：
2006
影响因子：
1
通讯作者：
J. Davies
中科院分区：
文献类型：
--
作者：
C. Marr;J. Davies
本文为通信顺序进程（CSP）语言定义了一种新的指称语义。语义位于CSP现有的跟踪和故障模型之间，提供了一个单例故障的非确定性的治疗。虽然语义并不代表全语言的一致性，但它足以用于非确定性过程的顺序测试。这种语义正好对应于Z和Object-Z中常用的数据细化概念：当相应的流程根据单例失败进行细化时，抽象数据类型也会被细化。该语义用于探索数据精化和过程精化之间的关系，并推导出一个合理且完整的数据精化规则。
This paper defines a new denotational semantics for the language of Communicating Sequential Processes (CSP). The semantics lies between the existing traces and failures models of CSP, providing a treatment of non-determinism in terms of singleton failures. Although the semantics does not represent a congruence upon the full language, it is adequate for sequential tests of non-deterministic processes. This semantics corresponds exactly to a commonly used notion of data refinement in Z and Object-Z: an abstract data type is refined when the corresponding process is refined in terms of singleton failures. The semantics is used to explore the relationship between data refinement and process refinement, and to derive a rule for data refinement that is both sound and complete.