2009 Fiscal Year Annual Research Report
離散ダイナミクスの流体化によるシステムの安全性検証
| Project/Area Number |
21500009
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
平石 邦彦 Japan Advanced Institute of Science and Technology, 情報科学研究科, 教授 (40251970)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小林 孝一 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (50452115)
|
|---|
| Keywords | 形式検証 / 形式手法 / ハイブリッドシステム / 実時間システム / 性能評価 |
|---|
| Research Abstract |
離散ダイナミクスの流体化に関する理論的基盤の確立を目的として,平成21年度は,以下の2つの研究課題について重点的に研究を行った。
1.述語抽象化計算の高速化に関する研究:ハイブリッドシステムの保証付き近似計算のアプローチとして,状態空間を与えられた述語集合により分割し,その上の離散的状態遷移で近似する述語抽象化の手法がある.しかし,述語により抽象化された状態空間は述語数の指数関数的な数の離散状態を含むため,計算の効率化が必要である.平成21年度は,箱抽象化(Box Abstraction)と呼ばれる最もよく用いられる述語抽象化手法に対して,述語抽象化計算の高速化手法に関する研究を行った.抽象状態間の遷移を直接計算するのではなく,拡張抽象状態と呼ばれる大領域間の遷移関係をまず求め,その結果を用いて抽象状態間の遷移関係を推論する方法を提案し,計算時間の大幅な削減を達成した.
2.パラメータ付きハイブリッドシステムの過渡状態に対する保証付き近似計算手法:流体化モデルは区間パラメータを含むハイブリッドシステムとして表現される.本研究では,与えられた流体化モデルに対し,初期状態から各時点における到達可能状態集合を逐次計算していくことにより安全性検証を行うことを想定しているが,このための方法として,常微分方程式の初期値問題の解法である区間法を用いる.区間法をハイブリッドシステムに適用する際に問題になるのがモード遷移(微分方程式の切り替え)の取り扱い方である.平成21年度は,モード領域の区間分割により区間の膨張を低減するための計算方法について検討した.さらに,分割された多数の小領域に対する遷移計算を効率的に扱うためのデータ構造および実装方法を開発した.
|
