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

点击翻译按钮获取中文摘要

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.