1996 Fiscal Year Annual Research Report
| Project/Area Number |
08780312
|
|---|
| Research Institution | Shizuoka Institute of Science and Technology |
|---|
Principal Investigator |
猪股 俊光 静岡理工科大学, 理工学部, 助教授 (30213193)
|
|---|
| Keywords | 形式的設計法 / 仕様記述 / 並列計算モデル / 線形論理 / ペトリネット / 構成的プログラミング |
|---|
| Research Abstract |
本研究では,並列プログラム設計法の開発,ならびにその方法に基づいた設計システムの実現を目的とした.研究は3つのステップに分けて実施し,それぞれ以下の結論を得た.
1.設計仕様を記述するための表現法の考案:設計仕様の表現法には,並列計算に固有な動作が記述できるなどの性質が要求される.そのため,並列計算のためのモデル概念としてはペトリネットを,要求・条件の形式的記述や妥当性判定のために論理式を用いることとした.具体的には,ペトリネットで表現される並列動作や計算資源などを記述するために,古典論理の枠組としてではなく,線形論理に基づいた仕様記述言語を考案した.
2.論理式による仕様の記述:ペトリネットと線形論理の対応関係を次のように定めることとした.プレースを命題(あるいは述語),トランジションを推論規則,トランジションの発火を推論規則の適用.これにより,仕様は,初期マ-キングを始式として,最終マ-キングを結論(を表す式)として表される.
3.仕様を実現するペトリネットの構成:論理式で記述された仕様の妥当性を構成的に証明することができるならば,そのときの証明からペトリネットが構成される.具体的には,証明の中に含まれる推論規則ごとにトランジションをもうけ,推論規則の上式の論理式を入力プレース,下式の論理式を出力プレースすることによりペトリネットが構成される.
現在,考案した設計法の有効性を確かめるために,設計システムの計算機上での実現を試みている.
今後の課題として,得られたペトリネットのもつ性質を検討,設計システムの実現があげられる.
|
