| 研究概要 |
本年度は,主として多数の並行プロセスとしてモデル化できる論理システムの検証を対象にし,論理システムの抽象化や分散検証アルゴリズムの研究を行い次のような成果を得た.
1.並行プロセスの検証:大規模論理システムでは比較的単純な動作を行うプロセスの並行動作としてシステム全体の動作を記述できる場合がある.このような論理システムの設計検証に適した検証アルゴリズムとして,検証のための像計算を行う前にプロセス変数をスムーズアウトする記号モデル検査法を提案し,従来の記号モデル検査法に対して10倍以上高速化できることを示した.
2.タスク制御アーキテクチャの検証:多数の並行プロセスとしてモデル化できる論理システムの例として,ロボット制御プログラムのモデルであるタスク制御アーキテクチャのデッドロックフリー性の検証を行った.並行プロセスのデッドロックフリー性の検証では,通常公平性制約のもとで検証を行う必要があるため非常に検証時間がかかる.これに対して,タスク制御アーキテクチャの性質に着目することにより,公平性制約を用いずにデッドロックフリー性の検証を行う方法を提案し,実際にこの手法により100倍以上高速化できることを示した.また,検証時間に大きく影響するタスクの順序付けに対し,分散ヒューリスティックアルゴリズムを示し,25台の計算機で分散処理を行った結果スーパーリニア効果が得られる場合もあることが判明した.さらに,タスク制御アーキテクチャの記述を容易に行うためのタスク制御アーキテクチャ入力支援システムの開発も行った.
|
