1998 Fiscal Year Annual Research Report
| Project/Area Number |
09680348
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
|
|---|
| Keywords | 設計検証 / 論理設計 / 形式的検証 / 時相論理 / 記号モデル検査 / 分散アルゴリズム / BDD |
|---|
| Research Abstract |
本年度は,主として多数の並行プロセスとしてモデル化できる論理システムの検証を対象にし,論理システムの抽象化や分散検証アルゴリズムの研究を行い次のような成果を得た.
1.並行プロセスの検証:大規模論理システムでは比較的単純な動作を行うプロセスの並行動作としてシステム全体の動作を記述できる場合がある.このような論理システムの設計検証に適した検証アルゴリズムとして,検証のための像計算を行う前にプロセス変数をスムーズアウトする記号モデル検査法を提案し,従来の記号モデル検査法に対して10倍以上高速化できることを示した.
2.タスク制御アーキテクチャの検証:多数の並行プロセスとしてモデル化できる論理システムの例として,ロボット制御プログラムのモデルであるタスク制御アーキテクチャのデッドロックフリー性の検証を行った.並行プロセスのデッドロックフリー性の検証では,通常公平性制約のもとで検証を行う必要があるため非常に検証時間がかかる.これに対して,タスク制御アーキテクチャの性質に着目することにより,公平性制約を用いずにデッドロックフリー性の検証を行う方法を提案し,実際にこの手法により100倍以上高速化できることを示した.また,検証時間に大きく影響するタスクの順序付けに対し,分散ヒューリスティックアルゴリズムを示し,25台の計算機で分散処理を行った結果スーパーリニア効果が得られる場合もあることが判明した.さらに,タスク制御アーキテクチャの記述を容易に行うためのタスク制御アーキテクチャ入力支援システムの開発も行った.
|
-
[Publications] 平石 裕実: "形式的論理設定検証およびメッセージ書換型プロキシサーバの研究" 京都産業大学計算機科学研究所報. 15・1. 47-51 (1998)
-
[Publications] 塚本 伸也: "タスク制御アーキテクチャ入力支援システム" 京都産業大学研鑽幾何学研究所報. (発表予定). (1999)
-
[Publications] 平石 裕実: "記号モデル検証システムSMVにおける像計算" 電子情報通信学会論文誌. (発表予定). (1999)
