一种从Object—Z到CSP规格说明的转化方法

面向对象形式规格说明语言Object-Z与进程代数CSP相结合是当今的一个热点,它既可以表示复杂的模块化数据与算法,又可以表示系统的行为,但求精与验证对它们结合后的规格说明需要分别进行处理。本文提出了一个方法,把Object-Z规格说明转化为CSP规格说明,可以方便地处理结合后的规格说明,因此求精与推理对结合后的规格说明可以按CSP规则与方法一致来进行处理。此外,转化后的Object-Z规格说明可以按照CSP方法进行模型检查。

An Approach to Translating Object-Z Specification to CSP Specification

Object-Z is an extension to the formal specification language Z, which facilitates specification in an object-oriented style and improves the clarity of large specifications through enhanced structuring. Object-Z is an excellent tool for modeling data and algorithms, but it is difficult to be used to capture the behaviour of concurrent reactive systems. CSP is good at modeling concurrent behaviour, but has little support for modeling the state of a complex system. The blending of Object-Z and CSP is a trend today, but the refinement and verification are taken apart for the blending speicification respectively, which is very inconvenient. This paper introduces an approach to translating the Object-Z specification to CSP specification, which is in favor of refinement and verification for the blending specification because refinement and verification can accord with the method of CSP uniformly. Moreover, conversional Object-Z specification can be model-checked according to that of CSP.