|
種々の量的時間制約を含む並行計算システムに対する形式仕様・形式検証の方法論を線形論理学的手法を用いて与えた。時間制約付き並行計算プロセスを線形論理の証明で記述することにより、論理学的な証明分析手法を実時間並行計算システムの仕様・検証理論に適用した。特に稠密時間の枠組における線形論理的分析法の有効性を示した。又、後半では、種々の具体的な実時間有限状態システムのサンプルに対して我々の仕様・検証の方法論を適応し、方法論の検討・評価を行った。まず実時間システムの具体例(例えば、交通網自動制御システムの形式仕様とその安全性検証、実時間制約つきPhilosopher's Table等)に我々の方法論を適用し、これまでの他の方法論と比較検討した。特に、マルチエージェントの数や時間制約が発展的に変化する並行計算システムの仕様・検証例を用いて、我々の方法論の独自性を考察した。
伝統的な方法論である、時間オートマタ(Timed Automata)によるモデルチェッキングと呼ばれる手法による検証も(PSPACE)決定的であることがこれまでに知られている。これら伝統的モデルチェッキング法との比較も行い、われわれの新しい論理的方法論の特徴を調べた、又、これまでのオートマタを用いたモデル化の段階でしばしば生じるValidationの問題(実時間システムの設計者の最初の意図通にモデル化がなされているかどうかを問う問題)に焦点を当て、われわれの論理的形式仕様の方法論のメリットを分析した。われわれの論理的形式仕様の方法論では、ある形式で記述された仕様から論理的仕様への自動変換が可能である。又自然な表示的意味論(trace semantics)との間で完全性定理が成り立っている。これらの理由により仕様記述の意味が正確に論理的仕様に反映されること、及びこのようなValidationの問題が生じないことを確認した。
|
