| 研究課題/領域番号 |
13558031
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 展開研究 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 慶應義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| 研究分担者 |
中川 中 (株)エスアールエー, ソフトウェア工学研究所, 部長
田村 直之 神戸大学, 工学部, 教授 (60207248)
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| 研究期間 (年度) |
2001 – 2003
|
| 研究課題ステータス |
完了 (2003年度)
|
| 配分額 *注記 |
6,700千円 (直接経費: 6,700千円)
2003年度: 1,900千円 (直接経費: 1,900千円)
2002年度: 2,000千円 (直接経費: 2,000千円)
2001年度: 2,800千円 (直接経費: 2,800千円)
|
|---|
| キーワード | 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論 |
|---|
| 研究概要 |
我々の形式仕様・検証ツールの設計と実装を進めた。又この仕様検証ツールを用いて、種々の実時間有限状態システムのサンプルに対して仕様、検証のケーススタディを行った。例えば実時間システムの研究分野でベンチマークとして使われている代表的な実時間システムの具体例(例えば、交通網自動制御システムの形式仕様とその安全性検証等)に我々の方法論を適用し、我々の論理的な方法論の有効性を検討した。特に、エージェントの数や時間制約が発展的に変化する並行計算システムの仕様・検証例を用いて、我々の方法論の独自性や特徴を示した。エージェントの数がダイナミックに変化する実時間システムの検証に対応するための実装の設計をフランス側共同研究グループと行った。まずユーザレベルで与えられた仕様は線形論理を用いた形式仕様に変換されグローバルな(例えば状態間の)時間制約をローカルタイマーを用いた時間制約に変換される。この時、この形式仕様レベルでは限定量化子等の意味はその時々の参加するエージェントの集合等に依存してダイナミックに変化することとなる。この形式仕様を使って効率的な検証を行う目的でエージェントの総数や各状態にあるエージェント数等をカウントするカウンターを用いた仕様への自動変換を行う。さらに稠密時間概念の消去手続きを行う。手続きの基礎となる基本定理は先行研究の中でKanovitch-Okada-Scedrovによって与えられていたが、この定理からアルゴリズムを抽出することにより安全性検証(reachability)のための稠密時間消去手続きの実装が行われた。又、このアルゴリズム抽出過程の分析を通じて安全性以外の(例えばAppointment problemや種々のスケジューリング)手続きへの拡張を行った。又、同様な方法論を用いてSecurity Protocolsの安全性検証を行う目的で、安全性検証のための論理推論体系の研究を進めた。又、我々の形式仕様検証言語として採用している線形論理の構文論と意味論に関する関連研究も進めた。
|
