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

并行计算系统规范和验证的代数方法

基本信息

批准号：
60550263
负责人：
INAGAKI Yasuyoshi
金额：
$ 1.28万
依托单位：
Nagoya University
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1985
资助国家：
日本
起止时间：
1985 至 1986
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-60550263/
关键词：
Parallel Computation System Concurrent System Algebraic Specification Method Verification of Specification CCS CSP Temporal Logic シストリックアルゴリズム

项目摘要

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.

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