A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems
A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems
复制标题
用于并发系统规范的 Object-Z 和 CSP 的语义集成
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Graeme Smith
中科院分区：
文献类型：
--
作者：
Graeme Smith
本文提出了一种使用面向对象的基于状态的规范语言Object-Z和进程代数CSP对并发系统进行形式化描述的方法。Object-Z提供了一种方便的方法来对复杂的数据结构进行建模，这些数据结构用于定义此类系统的组件过程，而CSP则能够对过程交互进行简明的说明。集成的基础是Object-Z类的语义，与CSP进程的语义相同。这允许在Object-Z中指定的类直接在规范的CSP部分中使用。
This paper presents a method of formally specifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to be used directly within the CSP part of the specification.