2014 Fiscal Year Research-status Report
動的システムに対する組込み制御プログラムの信頼性検証に関する研究
| Project/Area Number |
26330092
|
|---|
| Research Institution | Nihon University |
|---|
Principal Investigator |
関澤 俊弦 日本大学, 工学部, 准教授 (10549314)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
岡野 浩三 信州大学, 工学部, 准教授 (70252632)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | モデル検査 |
|---|
| Outline of Annual Research Achievements |
平成26年度は，フィードバック制御の一つであるPID制御や外乱を導入したシステムのモデル化および検証を目的としていた．この目的に対して，流量制御を行なう水槽を対象としてモデル検査器SPINの記述言語であるPromelaを用いてモデル化を行なった．作成したモデル群では，外乱を含んだ系に対してもモデル検査器上のシミュレーションでは良好な結果が得られた一方，状態数爆発問題により検証が困難となる場合が生じた．この問題の解決を目的として，抽象化手法の適用によりこの問題の解決を図っている．また，シミュレーション結果に基づく状態数削減手法を検討している．
上記課題における外乱を導入したモデル化の結果に基づき，平成27年度に予定されていた課題である確率的な振舞いをする系のモデル化および検証にも平成26年度に合わせて着手した．本課題に対しては，確率的な振舞いを示す自律移動ロボットの振舞いをマルコフ決定過程(Markov Decision Process)で表現可能であることを示した．また，確率モデル検査器PRISMを用いて外乱を含む自律移動系をモデル化し，外乱で挙動が乱される系に対して到達可能性などの性質を検証可能であることを確認した．この実績は現時点で国際会議に投稿済みであり，査読結果待ちとなっている．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
フィードバック制御および外乱を導入した系に関しては，モデル検査の記述言語を用いて連続量を離散化した形式的なモデルを作成した．これらのモデルは，対象の系の振舞いを良好にシミュレーション可能であることを示した．一方，抽象化手法が適切でなかったため状態数爆発を十分に抑えられなかったことにより，部分的な検証に留まっている．
上記課題への取組みで得られた外乱の扱いに基づき，平成27年度に予定されていた確率系の検証に関する課題を前倒しで開始した．この課題に関しても確率的な振舞いを持つ自律系を移動範囲の領域を区間分割する手法により，連続量を離散化してモデル化可能であることを示した．また，確率モデル検査器のモデル記述言語を用いてモデル化を行ない，到達可能性など一定の振舞いを検証可能であることを示した．この課題に関しては前倒しで実施していることから計画よりも進展していると言える．
これらの結果から，課題の実施に必要となる基礎的な研究要素に関する研究は進展しているが，全体の進展としてはやや遅れていると評価した．
|
| Strategy for Future Research Activity |
平成26年度において課題遂行に必要となる研究要素は一定の進展があったと判断している．これらの結果に基づき，平成27年度は，フィードバック制御，確率系および外乱を含む系のモデル化を検証を進める．問題となっている抽象化は，確率系の課題で効果があった区間分割手法をシミュレーションを併用することにより研究を進める予定である．
また，平成27年度は上記の結果に基づき，離散系と連続系が混在するハイブリッドシステムの検証を進める予定である．
研究代表者が平成26年4月，研究分担者が平成26年3月に異動により所属が変わったため，変換ツールの実装などを担当する予定であった大学院生の研究体制に再考が必要となっている．研究代表者が所属する研究室で大学院に進学予定の学生，または，研究分担者の所属する研究室の大学院生が新たな候補者である．
|
| Causes of Carryover |
使用額に差異が生じた直接的な理由は，申請時に演算用環境として計上したノートPC2台を1台のみの購入としたためです．これは，平成26年度4月に研究代表者が異動したため，課題遂行に必要となる旅費等の見込み額が変わり，ノートPCの購入可否を検討していたためです．
|
| Expenditure Plan for Carryover Budget |
平成26年度ではノートPC1台の購入を平成27年度に繰り越しましたが，研究課題遂行のために演算環境が必要である状況に変わりはないため，平成27年度の早い時期に購入予定です．
また，平成27年度には，Mathematica(192千円×2)の購入を申請していましたが，研究の進展に伴い，Matlab/Simulink(180千円*2，税抜)の方が適切であると考えています．上記の演算環境と合わせて購入予定です．
|
Research Products
(2 results)
