時間制約付きペトリネットモデルで記述された分散システムの動作仕様の自動導出

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

1.申請者らの論文"Synthesis of Protocol Entities'Specifications from Service Specifications in a Petri Net Model with Registers",Proc.of 15th IEEE International Conference on Distributed Computing Systems,pp.510-517,(1995-6).で実用的なシステムを記述するのに(時間制約を考慮にいれていないことを除いて)ほぼ充分なクラスで自動導出ができる方法を考案した.2.このクラスに対して時間制約を付加したモデルを考案した.具体的には,時間制約のモデルとして一般的なTimed Petrinetのモデルを我々のモデルに取り込むこととした.このモデルでは,時間制約として,トランジションの発火可能な状態から実際に発火するまでの最小時間と最大時間を与えている.3.このモデルとクラスのもとで,通信に一定の最大時間遅延が与えられた分散環境での実行可能性判定アルゴリズムを考案した.実行可能性の判定問題は,実数数上の線形制約式として与えられるように工夫したため,実用的な問題が十分に解ける.4.実行可能性がある際の動作仕様導出アルゴリズムを考案した.分散環境下の各実行ノードが十分に正確な内部時計を持っているという仮定のもとで,もとの仕様通りに動作する動作仕様を導出する.この動作仕様導出アルゴリズムで生成される動作仕様は一般的に時間遅延をなるべく押さえることができる.また,分散環境下での実行選択や,レジスタ値の更新競合をメッセージに時刻印を持たせる方法で解決可能であることを示した.また,本システムの導出系を作成した.5.以上の成果を平成8年3月26日に電子情報通信学会ソフトウェアサイエンス研究会にて発表する(予定).今後は,いくつかの制約条件を緩めたうえで,国際会議(ICDCS'97等)の投稿を予定している.