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

计算机科学 ›› 2006, Vol. 33 ›› Issue (11): 263-267.

• 计算机网络与信息安全 • 上一篇下一篇

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

文志诚缪淮扣许庆国

上海大学计算机学院,上海200072

出版日期:2018-11-17 发布日期:2018-11-17
基金资助:
国家自然科学基金（60373072）和上海市教委第四期重点学科建设基金资助.

WEN Zhi-Cheng ,MIAO Huai-Kou, XU Qing-Guo （School of Computer Engineering and Science, Shanghai University, Shanghai 200072）

Online:2018-11-17 Published:2018-11-17

摘要/Abstract

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

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

Abstract: 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

Key words: Object-Z, CSP, Formal specification, Parameterized process, Conversion

文志诚缪淮扣许庆国. 一种从Object—Z到CSP规格说明的转化方法[J]. 计算机科学, 2006, 33(11): 263-267. https://doi.org/

WEN Zhi-Cheng ,MIAO Huai-Kou, XU Qing-Guo （School of Computer Engineering and Science, Shanghai University, Shanghai 200072）. [J]. Computer Science, 2006, 33(11): 263-267. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

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

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

Metrics

本文评价

推荐阅读 0