2016 Fiscal Year Annual Research Report
A research on verification of embedded control program for dynamic systems
| 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 |
本研究課題は，組込みシステムにおいて確率的な振舞いを示す系を対象としている．本研究課題では，自律移動ロボットを具体的な対象事例としている．自律移動ロボットは，センサを用いてシステム外の情報を収集するが，センサの誤差や外乱などにより不確定性がある．本研究課題では，自律移動ロボットの振舞いを形式的および定量的に扱うために，そのモデル化および検証に取り組んでいる．このような不確定性を含む系は，自律移動ロボットに限らずCPS (Cyber Physical System) に用いられる組込みシステムの品質評価に繋がる．
平成27年度までに，確率的な振舞いは区間分割などの手法によりマルコフ決定過程として扱えることが判明していた．しかし，現実的な自律移動ロボットの振舞いを考えるとき，自己位置推定手法の形式的な扱いや時間に関する振舞いも重要である．自己位置推定についてはマルコフ位置推定を離散的に扱い，確率を排除したモデルで自己位置の検証が可能であることを示した．確率が考慮されていない点に課題が残るが，モデル化の手法は今後の拡張に繋がると考えられる．また，時間的な性質をモデル化するために，確率時間オートマトンを適用することにより，確率的な性質と時間的な性質を併せ持つ形式的なモデルを構築できることを示した．
本研究課題の研究計画では，自律移動ロボットをハイブリッドシステムとして扱うことを想定していた．しかし，自己位置推定を含む確率的および時間的性質を持つ確率ロボティックスを対象とする場合，時間を連続量として扱い，他の性質は可能な限り離散的に扱うことにより，その性質を検証可能であることを示した．
|
