2022 Fiscal Year Annual Research Report
Software adaptation with reasonable compromise using information on deductive proof of consistency
| Project/Area Number |
19K20249
|
|---|
| Research Institution | Japan Aerospace EXploration Agency |
|---|
Principal Investigator |
小林 努 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | ソフトウェア / 形式手法 / システムモデリング / 段階的詳細化 / 定理証明 / Event-B / 自動運転 / RSS |
|---|
| Outline of Annual Research Achievements |
変化する複雑な環境の中で動作する、高い安全性が求められるソフトウェアの需要が増加している。これに対し、動作環境と制御器の動作を形式的な仕様で記述して検証するアプローチが有効だが、現実の環境には開発時の想定と違う振る舞いや変化が存在する。そこで、本研究では、環境が変化した際に、要求を満たすように整合性のある形で制御器を適切に変更(適応)することで、実世界で動くソフトウェアの安全性向上に寄与することを目指した。
2022年度においては、自動運転車を対象として、既存の安全アーキテクチャ(Simplex architecture)を用いた制御器のモデルの構築・検証手法を提案した。この制御器には研究代表者が開発に関わった適応ルールが組み込まれている。ここでは達成目標と振舞いを定めたときに、特定の前提のもとで安全性と目標達成が両立できることが数学的に保証されており、この前提を環境の状態と比較することで適切な適応が可能になる。また、安全アーキテクチャを用いることにより、高い性能を得るためのブラックボックス制御器（機械学習を用いたものなど）を持つ制御器に対しても安全性と目標達成を確実にする適応が可能になっている。このように、現実的な問題に対する制御器の安全・適切な適応に寄与することができた。
期間全体を通じて、複雑な環境の中で動作するソフトウェアについて、パターンを用いた特定の変化に対応する制御器の自動変換、妥協の必要性や対応可能な変化の限界に関する分析、現実的な問題に対する適応機構の検証のための手法を提案できた。
|
Research Products
(4 results)
-
-
[Journal Article] Goal-Aware RSS for Complex Scenarios Via Program Logic2022
Author(s)
Hasuo Ichiro、Eberhart Clovis、Haydon James、Dubut Jeremy、Bohrer Rose、Kobayashi Tsutomu、Pruekprasert Sasinee、Zhang Xiao-Yi、Pallas Erik Andre、Yamada Akihisa、Suenaga Kohei、Ishikawa Fuyuki、Kamijo Kenji、Shinya Yoshiyuki、Suetomi Takamasa
-
Journal Title
IEEE Transactions on Intelligent Vehicles
Volume: (to appear)
Pages: 1～33
DOI
Peer Reviewed / Int'l Joint Research
-
-
