My PhD Thesis

Title

A Programming Environment for Reactive and Concurrent Systems Using Petri Nets and Temporal Logic
（ペトリネットと時相論理を用いた リアクティブ並行システムの開発環境の研究）

Abstract

There has been a rapid trend towards parallel, distributed, and interactive/reactive computing over the past decade. Generally speaking, it is not so easy for ordinary programmers to produce correct and efficient programs for these systems as compared with sequential programming. Therefore, some kind of computer-aided concurrent programming environment is necessary to achieve high productivity and high reliability. The purpose of this thesis is to present theories, methods and tools (programming environments) for reactive and concurrent systems using Petri nets and temporal logic.

Both Petri nets and temporal logic have been investigated as formal specification languages for reactive and concurrent systems. While temporal logic is appropriate for specifying the properties and constraints of programs but inappropriate for specifying the behavioral structures of programs, Petri nets can specify the behavioral structures but not the properties and constraints. In this thesis, the fusion of Petri nets and temporal logic is proposed as a specification language for reactive and concurrent systems. Then, practical and efficient verification and synthesis methods using Petri nets and temporal logic and Petri-net-based design methodology are described. Finally, a programming environment embedding these methods is introduced. This thesis attempts in illustrating a typical programming paradigm and its environment using Petri nets and temporal logic.

The main outcomes of this thesis are as follows.

• Specification by fusion of Petri nets and temporal logic
  The fusion of Petri nets and temporal logic is proposed as a specification language, and its applications to verification and synthesis are considered. The remarkable point is that the proposed methods are for unbounded Petri nets, while former verification and synthesis methods were mainly for bounded (i.e., finite) ones.
• Compositional verification
  An efficient and practical verification method using transition systems (bounded Petri nets) and temporal logic is proposed. Generally, the computation costs for verification increase exponentially as the scale of the programs increases. To overcome this problem, a reduction technique of the target program has been investigated using bisimulation equivalence. However, bisimulation equivalence cannot deal with ``divergence'' explicitly. Therefore, a new process equivalence relation ($\pi\tau\omega$-bisimulation equivalence) is proposed. A Process Query Language (PQL) which is an extended temporal logic and semantics of which is based on $\pi\tau\omega$-bisimulation equivalence is defined. Then, a compositional verification method using PQL is proposed.
• Compositional program adjustment
  A new synthesis method using transition systems (bounded Petri nets) and temporal logic is proposed. Since conventional program generation from a temporal logic specification is impractical, this thesis proposes a new approach, ``program adjustment''. In program adjustment, a target program written by programmers which may be functionally correct but may be imperfect in its timing is automatically adjusted (tuned up) to satisfy given temporal logic constraints.
• Petri-net-based software design methodology
  A Petri-net-based software design method is proposed. In this method, a causality matrix is introduced for an earlier design phase when the system structure is obscure and it is difficult to write Petri nets directly. A designer can construct Petri nets systematically from an ambiguous requirement using the causality matrices according to the design method.
• MENDELS ZONE
  A programming environment, MENDELS ZONE, based on the above techniques has been developed. MENDEL net which is a high-level Petri net for reactive and concurrent systems is used as the programming language. The designer constructs a program (MENDEL net) and verifies it using temporal logic. If there are any bugs, the program can be adjusted. Finally, the constructed program is executed on a parallel computer.

計算機システムの並列化，分散化，インタラクティブ/リアクティブ化に伴い， 並行プログラミングの需要はますます大きくなりつつある．しかしながら，並 行プログラムの開発は，逐次プログラムの開発に比べて格段に難しい．さらに， 制御システムなどのリアクティブシステムの並行プログラムには高い信頼性が 要求されることが多い．このようなソフトウェアの高生産性および高信頼性を 確保するためには，ソフトウェア開発の計算機支援は不可欠である．本研究の 目的は，ペトリネットと時相論理を用いたリアクティブ・並行システムのソフ トウェア開発支援技術を確立することである．

ペトリネットと時相論理はともに並行システムの形式的な仕様記述法とし て研究されてきた．しかし，時相論理は制約記述には適しているが構造記 述には不適であり，逆にペトリネットは構造記述には適しているが制約記 述には不適であった．そこで，本研究では時相論理とペトリネットの融合 によるリアクティブ・並行システムの仕様記述法を採用する．さらに，ペ トリネットと時相論理を用いた実用的な検証・合成手法などの要素技術を 開発し，それらを組み込んだプログラムの開発環境の試作およびソフトウェ ア設計方法論の提示を行なう．本研究により，ペトリネットと時相論理を 用いた一つの具体的なソフトウェア開発支援体系を確立することができた．

本研究の主な具体的成果としては，以下の項目がある．

• ペトリネットと時相論理の融合による仕様記述法の提案
  時相論理とペトリネットの融合法を示し，ペトリネットが時相論理を満た すか否かを検証するアルゴリズムを示した．従来，有界なペトリネットに 対する時相論理による検証法は知られていたが，それを有界でない一般の ペトリネットの検証に拡張した．
• 積み重ね式検証法の研究
  遷移システム(有限ペトリネット)と時相論理を用いた大規模プログラムに 対する効率的な検証法を示した．従来，時相論理のモデル検査法では検証 に要するコストの爆発的増大が問題あり，これを回避するために様々な方 法が提案され，その１つに検証対象の縮約手法がある．しかし，従来の方 式では，「内部遷移による無限ループ」の処理に関して問題があった．本 研究では，その問題点を指摘するとともに，それを是正する新しい様相論 理PQLを提案し，PQLを用いた積み重ね検証法を示した．
• プログラム調整法の研究
  遷移システム(有限ペトリネット)と時相論理による並行プログラムの新し い合成法を示した．従来の時相論理からのプログラム合成法は，実用規模 のプログラムに適用するには仕様記述能力および計算量の点で非現実的で あった．そこで，プログラム全体の自動合成ではなく，人間が作成した不 完全なプログラム(遷移システム)を時相論理式で記述された仕様を満たす ように部分的に自動修正し，目的のプログラムを生成する「プログラム調 整法」を提案した．
• ネット指向ソフトウェア設計法の提案
  ペトリネットは単なる記述手段であり，あいまいな仕様からペトリネット を導出するためのガイドライン(設計法)が必要である．本研究では，あい まいな仕様をペトリネットに具体化する手段として因果関係マトリックス を導入したリアクティブ・並行システムのソフトウェア設計法を提案した．
• プログラミング環境MENDELS ZONEの開発
  上記の要素技術を統合したプログランミング環境を並列計算機上に試作し た．ここで，プログラムは高水準ペトリネットであるMENDELネットで記述 する．設計者はネット指向設計法によりプログラム(MENDELネット)を作成 し，プログラム検証でプログラムを検証し，もし問題点がある場合はプロ グラム調整によりプログラムを改善する．さらに，生成されたプログラム を実際に並列マシン上で実行できる．

博士論文書誌データベース

項目 内容 
書誌ID 000000329905 
学位取得者名 内平直志 
学位取得者名よみ ウチヒラ,ナオシ 
学位取得者名(英字) UCHIHIRA N 
タイトル A Programming Environment for Reactive and Concurrent Systems Using Petri Nets and Temporal Logic
(ペトリネットと時相論理を用いたリアクティブ並行システムの開発環境の研究) 
学位授与大学コード 0028 
学位授与大学名 東京工業大学 
学位授与大学名(英語) Tokyo Institute of Technology 
取得学位 博士(工学) 
取得学位(英語) Engineering 
報告番号 乙第3125号 
学位授与年月日 平成9年12月31日 
学位授与年 1997 
分類法の種類 国立国会図書館分類表 
分類記号 UT51 

Download

Naoshi Uchihira, Dr. Eng.