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) < ω >的代数-正则表达式：我们提出了一个闭正则表达式的公理系统。获得CCS方程的显式解形式，揭示解与封闭正则表达式之间存在的关系，是今后的研究课题。(3)并行系统的代数规范方法：我们提出了一种并行系统的代数规范方法CCS/ADT，该方法将值的域作为抽象的数据类型，并对其进行代数描述。CCS/ADT中规范的语义由带有状态的通信树给出。(4)通信协议的规范与验证方法：利用麦克德莫特时间逻辑，开发了通信协议的规范与验证方法。我们也在Prolog中实现了它。(5)我们开发了收缩算法的形式化描述和实现方法。

项目成果

村上昌己: 電子通信学会論文誌. J69-D. 190-197 (1986)

村上正美：电子与通信工程师协会学报 J69-D 190-197 (1986)。

Hirotomo ASO: "Formal Description of Systolic Algorithms and an Analysis of the Information Flow" The Transactions of the Institute of Electronics, Information and Communication Engineers. J70-D. (1987)

Hirotomo ASO：“脉动算法的形式化描述和信息流分析”电子、信息和通信工程师学会汇刊。

稲垣康善: 情報処理. 27. 120-128 (1986)

Yasuyoshi Inagaki：信息处理。27. 120-128 (1986)

Hidehiko KITA: "Algebraic Specification Method of Programming Languages" The Transactions of the Institute of Electronics, Information and Communication Engineers. J70-D. 247-258 (1987)

Hidehiko KITA：“编程语言的代数规约方法”电子、信息和通信工程师学会会刊。

Yasuyoshi INAGAKI: Ohm Co.Software Engineering Handbook, Chapter 3 (H. Enomoto ed.), pp.51-91 (1985)

Yasuyoshi INAGAKI：Ohm Co. 软件工程手册，第 3 章（H. Enomoto 编辑），第 51-91 页 (1985)