並列プログラムの形式的設計法とその実現

点击翻译按钮获取中文摘要

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