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

本课题的研究目的是了解如何制定一种具有足够形式化、可构造性、可理解性和简单性的并发或并行计算系统的规范和验证方法。本课题的主要研究成果有：(1)通信顺序进程部分正确性和无死锁验证系统：通过集中式方法给出的计算历史集定义了通信顺序进程（CSP）的语义。基于语义，我们提出了一种类似hoare的CSP部分正确性和无死锁验证系统。我们已经证明了这个制度的合理性。(2) < ω >的代数-正则表达式：我们提出了一个闭正则表达式的公理系统。获得CCS方程的显式解形式，揭示解与封闭正则表达式之间存在的关系，是今后的研究课题。(3)并行系统的代数规范方法：我们提出了一种并行系统的代数规范方法CCS/ADT，该方法将值的域作为抽象的数据类型，并对其进行代数描述。CCS/ADT中规范的语义由带有状态的通信树给出。(4)通信协议的规范与验证方法：利用麦克德莫特时间逻辑，开发了通信协议的规范与验证方法。我们也在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.