A Research on property generation for embedded systems based on combination testing methodology
| Project/Area Number |
17K00111
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Nihon University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
岡野 浩三 信州大学, 学術研究院工学系, 准教授 (70252632)
見越 大樹 日本大学, 工学部, 講師 (00634114)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Project Status |
Completed (Fiscal Year 2019)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2018: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2017: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
|---|
| Keywords | モデル検査 / 確率系 / ロボティックス / アドホックネットワーク / 自己位置推定 / ゲートウェイ配置 / 情報工学 / 形式検証 / 検査項目生成 / 仕様記述 |
|---|
| Outline of Final Research Achievements |
This research is a study of a method to ensure reliability of cyber physical systems that correct external information using sensors, by applying model checking technique which is one of reliability ensuring techniques for information systems. For this purpose, we set systems based on robotics and ad-hoc networks with uncertainty behaviors, as concrete targets. We applied model checking technique and property generation to systems based on self-localization algorithm, and showed reliability can be ensured by our proposed approach. As a result, it is possible to construct systems which show expected behaviors. Additionally, we showed a method to feed back to systems by applying analysis results of counter example that is an evidence that the expected property does not hold, when the systems exhibits undesired behaviors.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究は，組込みシステムの一つであるロボット制御やアドホックネットワーク環境において，ロボットやデバイスなどの移動体に加えて外部環境を含めて検証を行なうことにより，自己位置推定を可能とする系の構築手法を示した．自律移動やネットワーク領域において，自己位置推定は要素技術の一つである．本研究はGPS機能を持たない対象を想定しており，GPSなどに頼らずに位置推定を実現できる手法を示している．これは，信頼性が保証される情報システムの構築に寄与すると考える．
|
Report
(4 results)
Research Products
(12 results)
