An Algebraic Approach to the Specification and Verification of Parallel Computation System

本研究课题的目的是了解如何开发一种并发或并行计算系统的规格说明和验证方法，该方法具有足够的形式性、可构造性、可理解性和简单性。（1）通信顺序进程的部分正确性和无死锁验证系统：我们通过集中式方法给出的计算历史集定义了通信顺序进程CSP（Communicating Sequential Processes）的语义。基于该语义，我们提出了一个类Hoare的CSP部分正确无死锁验证系统。我们已经证明了这个系统的可靠性。(2)正则表达式的代数<omega>：我们提出了一个封闭的正则表达式的公理系统。得到CCS方程的显式解形式，并揭示其解与闭正则表达式之间的关系，是今后的研究课题。(3)并发系统的代数规格说明方法：我们提出了并发系统的代数规格说明方法CCS/ADT，在该方法中，我们将值的域作为抽象数据类型来把握，并对它们进行代数描述。CCS/ADT中规范的语义由带状态的通信树给出。(4)通信协议的描述和验证方法：我们利用McDermott的时序逻辑，提出了一种通信协议的描述和验证方法。我们也在Prolog中实现了它。(5)我们发展了脉动算法的形式化描述和实现方法。

The purpose of this research project is to know how to develop a specification and verification method of concurrent or parallel computation systems, which has enough formality, constructibility, comprehensibility and simplicity. Main results of this research project are :(1) Verification System for Partial Correctness and Freedom from Deadlock of Communicating Sequential Process : We have defined the semantics of CSP (Communicating Sequential Processes) by the set of computation histories, given by the centralized approach. Based on the semantics, we have proposed a Hoare-like verification system of partial correctness and freedom from deadlock of CSP. We have proved the soundness of the system.(2) An Algebra of <omega> -Regular Expression : We have proposed an axiom system of the closed regular expression. It is left as a future research problem to obtain an explicit solution form of equations of CCS and to reveal the relations existing between the solution and the closed regular expression.(3) Algebraic Specification Method of Concurrent System : We have proposed an algebraic specification method for concurrent systems, named CCS/ADT, in which we have grasped the domains of values as abstract data types and describe them algebraically. The semantics of the specification in CCS/ADT in given by the communication tree with states.(4) Specification and Verification Method of Communication Protocal : We have developed a specification and verification method of communication protocol by using McDermott's temporal logic. We have also implemented it in Prolog.(5) We have developed the methods of the formal description and implementation of systolic algorithms.