2015 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 |
平成27年度は，確率的な振舞いをもつ系のモデル化および検証を目的としていた．この目的に対して，平成26年度のモデル検査器SPIN上でのシミュレーションから，抽象化手法等の適用により状態数爆発を回避する必要があることが判明していた．この結果を受け，平成27年度には，本質的に連続量となる確率系に対して区間分割などの手法を適用しすることにより，状態数を抑制しつつマルコフ決定過程(Markov Decision Process)でモデル化が可能であることを示した．また，自律移動ロボットの実装例を具体的な対象として，確率的な振舞いが確率モデル検査で検証可能であることを示した．
上記の検証は，外乱を考慮した自律ロボットの誤差補正を対象としていた．しかし，自律移動ロボットの振舞いを考えたとき，自己位置推定などの要素技術が存在する．これらの要素技術に関してもモデル化および検証に着手し，確率的な振舞いを除いた系でモデル検査の適用可能性を示した．
提案手法の適用領域を拡張するためには確率的な性質のみならず，時間的な性質も考慮に入れる必要がある．そのため，時間的な性質のモデル検査における抽象化と反例解析手法の研究を行なった．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成27年度に取り組む課題とされていた確率系の研究要素は，区間分割等の手法を適用することより，本質的に連続となる確率分布を離散的な状態に落とし込みモデル化が可能となった．また，外乱を含んだモデル化も実現している．これらのモデルには一定の制約があるものの，自律移動ロボットを対象としたモデル検査を用いた検証が可能であることを示した．また，対象系の組込みシステムを離散系と連続系が混在するハイブリッドシステムと捉えたときの検証に対しては，まず時間的な要素の扱いに取り組んだ．モデル検査の際に問題となる状態爆発問題を回避するために，時間的要素を扱う反例解析手法に取り組み，状態数削減に効果があるこを示した．研究対象領域の拡張に必要となるこれらの確率的および時間的要素の取り組みと，現実的な自律移動ロボットで考慮が必要となる外乱の扱いに対して，モデル検査を用いた検証手法を提案したことにより，おおむね予定通り進展していると判断した．
|
| Strategy for Future Research Activity |
確率系の検証において，現在，モデル化は人手で行なっている．しかし，この方法は人為的な誤りが混入するだけでなく，体系化されていない点に問題がある．これまでの取り組みから半自動的なモデル化を実現するための変換ルールを策定することにより，特定の性質を満たす自律移動ロボットのモデル検査手法の体系化に取り組みたい．また，具体的な自律移動ロボットを考えたとき，外乱や位置の確率的分布などは観測データに基づく必要がある．平成27年度に，LEGO EV3を用いて自律移動ロボットを実装したことにより，誤差の確率分布などが測定可能となっている．平成28年度は，これらの観測データを活用することにより，より現実的な振舞いに対して提案手法が適用可能であることを示す予定である．また，時間的な性質を含めた連続量をモデルに取り込むことにより，提案手法の拡張を試みる．この試みでは，モデル検査だけでなくシミュレーション等の協調が必要と考えられる．
|
| Causes of Carryover |
使用額に差異が生じた理由の1つとして，成果を論文誌に投稿するにあたり別刷り代などを保留したことと，平成27年度に研究分担者が異動したため，設備や旅費等の見込み額が変わったためです．また，平成26年度は，研究の進捗と照らし合わせMatlab/Simulinkの購入を見送ったことも一因です．
|
| Expenditure Plan for Carryover Budget |
研究代表者および分担者の異動により旅費が申請時より増加する見込みであることと，研究計画で予定されている学会発表等に使用予定です．確率系などの信頼性保証においては，検証のみではなく，設計やシミュレーションの数値演算との組み合わせもアプローチの1つです．自律ロボットの実装により得られたこれまでの進捗を考えると，設計および解析用に平成27年度に購入を見送ったMatlab/Simulinkを購入する予定です．
|
