An Algebraic Approach to the Specification and Verification of Parallel Computation System
| Project/Area Number |
60550263
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機工学
|
|---|
| Research Institution | Nagoya 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)
|
|---|
| Keywords | Parallel 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)
Research Products
(13 results)
