• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 60550263
Research Category

Grant-in-Aid for General Scientific Research (C)

Allocation TypeSingle-year Grants
Research Field 計算機工学
Research InstitutionNagoya University

Principal Investigator

INAGAKI Yasuyoshi  Faculty of Engineering, Nagoya University, 工学部, 教授 (10023079)

Co-Investigator(Kenkyū-buntansha) SAKABE Toshiki  Faculty of Engineering, Mie University, 工学部, 助教授 (60111829)
ASO Hirotomo  Faculty of Engineering, Nagoya University (Faculty of Engineering, Tohoku Univer, 工学部(昭和61年10月より東北大学・工学部), 助教授 (10005522)
Project Period (FY) 1985 – 1986
Project Status Completed (Fiscal Year 1986)
Budget Amount *help
¥2,000,000 (Direct Cost: ¥2,000,000)
Fiscal Year 1986: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 1985: ¥1,000,000 (Direct Cost: ¥1,000,000)
KeywordsParallel Computation System / Concurrent System / Algebraic Specification Method / Verification of Specification / CCS / CSP / Temporal Logic / シストリックアルゴリズム
Research Abstract

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.

Report

(1 results)
  • 1986 Final Research Report Summary
  • Research Products

    (13 results)

All Other

All Publications (13 results)

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

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 村上昌己: 電子通信学会論文誌. J69-D. 190-197 (1986)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Kita,H.: Lecture Notes in Computer Science. 220. 144-157 (1986)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 北英彦: 電子情報通信学会論文誌. J70-D. 247-258 (1987)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 三浦大祐: 電子情報通信学会論文誌. J70-D. (1987)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 阿曽弘具: 電子情報通信学会論文誌. J70-D. (1987)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 稲垣康善著.榎本肇 編: "ソフトウェア工学ハンドブック 第3章" オーム社, 51-91 (1985)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Yasuyoshi INAGAKI: "Concept of Abstract Data Type and its Specification" Journal of Information Processing (Joho Shori). 27. 120-128 (1986)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Masaki MURAKAMI: "Verification System for Freedom from Deadlock of Communicating Sequential Processes" The Transactions of the Institute of Electronics and Communication Engineers of Japan. J69-D. 190-197 (1986)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Hidehiko KITA: "Algebraic Specification Method of Programming Languages" The Transactions of the Institute of Electronics, Information and Communication Engineers. J70-D. 247-258 (1987)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 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)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Daisuke MIURA: "A Synthesis Method of Systolic Algorithms for Nested Loop Programs" The Transactions of the Institute of Electronics, Information and Communication Engineers. J70-D. (1987)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Yasuyoshi INAGAKI: Ohm Co.Software Engineering Handbook, Chapter 3 (H. Enomoto ed.), pp.51-91 (1985)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary

URL: 

Published: 1987-03-31   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi