一种从object—z到csp规格说明的转化方法

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