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

• 作者: 文志诚 缪淮扣 许庆国
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: Object-Z CSP 形式规格说明 参数化进程 转化
• 年，卷（期）: 2006,（11）
• 所属期刊栏目: 软件工程
• 页码范围: 263-267
• 页数: 5页
• 分类号: TP3
• 字数: 6228字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2006.11.075

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	缪淮扣	上海大学计算机学院	100	1030	16.0	26.0
2	文志诚	上海大学计算机学院	4	21	3.0	4.0
3	许庆国	上海大学计算机学院	9	35	4.0	5.0