著者

西村 一彦 内平 直志

雑誌

全国大会講演論文集

巻号頁・発行日

vol.38, pp.1294-1295, 1989-03-15

---

並列プログラムの実行過程の解明や知能ロボットの行動計画生成問題は時間的関係を含んだ問題として定式化され,その方法として時制命題論理(PTL:Propositional Temporal Logic)による解決が試みられている.このようなPTLをベースとした具体的システムでは,論理式を形式的な仕様とみなし,仕様を満たすような手順系列を自動的に生成することができる.また,PTLで書かれた仕様が正しければ,その結果得られる手順系列も正しいことが保証されている.しかし,PTLによって記述された仕様(論理式)自体に誤り,不足がある場合は当然のことながらその結果も誤りとなる.ところが,結果の検証,デバッグはいまだに人手で行なわれている.バグとしては,(1)記述ミス(スペルミス),(2)きつい仕様(無駄な制約),(3)仕様が記述不足(制約が不足),を考える.(1)は原子命題や論理記号の記述ミスである.(2)では,無駄な制約のために,結果として得られるモデル集合(M)がユーザーが実行したいもの(U)に比べ小さなもの,すなわち,M⊆Uとなる.従って,MをUによって検証すれば必ず矛盾が発生し,その矛盾点を追跡することでバグを発見することができる.ところが,(3)は必ずしも検証過程で矛盾を引き起こすとは限らない.なぜなら,M⊇Uだからである.この場合,むしろ,不足している仕様が何であるかをユーザーから与えられるモデルから生成する機能が必要となる.そこで,(3)以外の二つのバグを同定する方法について述べる.まず,ここで対象とするPTLとその決定手続きであるタブロー法について解説し,PTL式のバグが何であるのかを定義する.次にユーザーモデルに基づいたバグの発見アルゴリズムについて詳述する.