| 研究概要 |
今年度の研究では、協調型言語による並列プログラムを対象として、安全性の線形時相論理に基づくモデル検証を試みた。結果としてin, out, rd操作を持つ各直列プロセスとタプル空間の組み合わせを対象としたモデル検証を行う際の1つの形式化ができた。さらに実験を通じてこの形式化の有効性を確かめた。
この形式化は具体的には以下の3つを対象とし、各項目にあげたような抽象化を行う。
1.タプル空間を、タプル空間内のタプルに関する論理式を原始論理式とするクリプケ構造とみなす。
2.プロセスをin, out, rd操作をアクションとするラベル付き遷移システム(LTS)とみなす。
3.プロセスをin, out, rd操作をアクションとする軌跡ともみなす。
モデル検証は調べたい性質を記述した時相論理式が成立するか否かを、有限状態機械(FSM)の状態空間を探索することによって調べる。クリプケ構造はその対象となるFSMであるが、一般に並列プログラムのモデル検証では各プロセスをモデル化したFSMの並列合成において状態空間の直積をとることにより"状態空間爆発"という問題が生じる。そこで検証の対象とする部分を1つのプロセス(LTS)とタプル空間(クリプケ構造)の通信に限り、他のプロセスとタプル空間との通信は軌跡を利用することにした。このときクリプケ構造と軌跡は前もって組み合わせておき、LTSとこの特殊な形のクリプケ構造による検証という形に帰着した。
最後に安全性の検証の実験を通して、特殊な形のクリプケ構造がちょうど失敗集合をなす拒絶集合と軌跡の組に似ていること、状態空間ではなく上の組み合わせによる問題が生じることを確かめたが、理論的根拠を示すにはいたっていない。
上の形式化の内容は応用数学合同研究集会で、さらに実験による検証を含めた内容は第1回ディペンダブルソフトウェアワークショップ(DSW2004)で口頭報告した。
|
