ペトリネット型実行制御部をもつ代数的仕様記述の検証と分散実行系

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

1.本研究では,複数の処理の並列実行や同期等が表現できる記述モデルとして次のモデルを考案した.実行制御をペトリネットで記述する.内部データを自然に扱えるよう,内部レジスタを有限個持つ.ト-クンの配置(マ-キング)だけでなく,内部レジスタ値に依存して次の動作が選択でき,また,一つの動作で,外部とのデータの入出力,及び,内部レジスタ値の更新ができる.(ICDCS'95)2.本モデルで記述した分散システムの全体仕様から,ネットワーク上で分散実行するプログラム群を自動導出する方法を考案した.得られるプログラム群では,動作効率の向上のため,ペトリネットモデルの利点を活かし,同時に発火可能なトランジションが複数並列に配置され,実行ステップ数が少なくなっている.また,プログラム間で交換されるメッセージ総数を,我々の過去の研究では一トランジションごと少なくしていたが,さらに,隣接する複数のトランジションの動作に着目し不必要なメッセージの削除を行なう工夫をしている.(信学論E77A-10,情処研報94-DPS65-27)また,本モデルのサブクラスであるステートマシンモデルに対する分散実行を視覚的に行なえる実行系を開発した.この実行系は同データ,音声等も扱え,グループウェアへの応用も可能となっている.(情処論文誌(採録))3.Kellnerのソフトウェアプロセスが本モデルで自然に記述できることを確かめた.また,この例題に対し,人間が効率を考慮に入れながら導出したものと比べ,本導出方法で遜色のない分散実行プログラムを得られることを確認した.(信学技報94-SS38)4.上述のステートマシンモデルの代数的な記述に対し,処理の正しさを証明する方法を考案した.また,整数上のある論理式の真偽判定法を利用する検証法を考案し,この真偽判定法を我々の検証システムに組み込んだ.(信学論SI(採録),TPCD'94)5.今後の課題として,本モデル上での安全性や生存性等の動的性質の検証方法と実行系の扱うクラスの拡張について検討したい.