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

An Approach to Translating Object-Z Specification to CSP Specification

作　　者：文志诚[1] 缪淮扣[1] 许庆国[1] 

机构地区：[1]上海大学计算机学院,上海200072

出　　处：《计算机科学》2006年第11期263-267,共5页Computer Science

基　　金：国家自然科学基金(60373072);上海市教委第四期重点学科建设基金资助。

摘　　要：面向对象形式规格说明语言Object-Z与进程代数CSP相结合是当今的一个热点,它既可以表示复杂的模块化数据与算法,又可以表示系统的行为,但求精与验证对它们结合后的规格说明需要分别进行处理。本文提出了一个方法,把Object-Z规格说明转化为CSP规格说明,可以方便地处理结合后的规格说明,因此求精与推理对结合后的规格说明可以按CSP规则与方法一致来进行处理。此外,转化后的Object-Z规格说明可以按照CSP方法进行模型检查。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. Ohject-Z is an excellent tool for modeling data and algorithms, but it is difficult to he used to capture the hehaviour 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, hut the refinement and verification are taken apart for the blending speicification respectively, which is very inconvenient. This paper introduces an approach to translating the Ohject-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 Ohject-Z specification can he model-checked according to that of CSP.

关 键 词：Object—Z CSP 形式规格说明 参数化进程 转化 

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]