Software adaptation with reasonable compromise using information on deductive proof of consistency
| Project/Area Number |
19K20249
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Japan Aerospace EXploration Agency (2022)
National Institute of Informatics (2019-2021) |
|---|
Principal Investigator |
Kobayashi Tsutomu 国立研究開発法人宇宙航空研究開発機構, 研究開発部門, 研究開発員 (10803405)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2021: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2020: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2019: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | 形式手法 / 段階的詳細化 / 定理証明 / 自己適応ソフトウェア / Internet of Things / 物理情報システム / AI安全性 / ソフトウェア / システムモデリング / Event-B / 自動運転 / RSS / 頑健性 |
|---|
| Outline of Research at the Start |
本研究では、3つの問題の解決のための手法を開発する。
第一に、「体系的に適切な適応を行うには？」という問題の解決のために、整合性を満たすような適応のパターンを定義する。
第二に、「適応時に賢く妥協するには？」という問題の解決のために、パターンに基づいて仕様の証明情報の分析手法を提案し満たせる要求の判断を体系化する。
第三に、「変化のあった側面のみに絞った適応を行うには？」という問題の解決のために、抽象化された仕様の上で行った適応を具体的な仕様に反映する手法を構築する。
|
| Outline of Final Research Achievements |
Mathematically proving the safety of software that controls things in the real world by using formally specified models of the controller and its environment provides a strong safety guarantee. In particular, specifying formal models in multiple abstraction levels (stepwise refinement) for reducing the complexity of modelling and verification has been attracting increased interest. In practice, however, there are gaps between the constructed environment model and the real environment. Therefore, after updating the environment model, developers should make adaptations to controller models so that the controller safely interacts with the real environment. We constructed methods for the adaptation to formal models in multiple abstraction levels, such as automatic robustification of the controller against perceptual uncertainty, safety architecture for autonomous vehicle software, and ensuring the safe recovery from faults of spacecraft.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究はコンピュータだけでなく人間にも理解・説明可能である形式的モデルの安全な変更・適応という工学的に発展中の工程に対し、多段階の抽象度の視点から切り込み成果を挙げた点で学術的に意義深いと考える。また、実世界で動作するソフトウェアシステムを（一部の研究ではAIを用いたブラックボックスシステムを）対象とし、その安全性を保証しつつ現実の開発問題に対処する手法を提供している点で社会的にも意義深いと考える。
|
Report
(5 results)
Research Products
(14 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)
Issue: 4
Pages: 1-33
DOI
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
