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