Software adaptation with reasonable compromise using information on deductive proof of consistency

2022 Fiscal Year Final Research Report

• 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
• Keywords: 形式手法 / 段階的詳細化 / 定理証明 / 自己適応ソフトウェア / Internet of Things / 物理情報システム / AI安全性

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.

Free Research Field

ソフトウェア工学

Academic Significance and Societal Importance of the Research Achievements

本研究はコンピュータだけでなく人間にも理解・説明可能である形式的モデルの安全な変更・適応という工学的に発展中の工程に対し、多段階の抽象度の視点から切り込み成果を挙げた点で学術的に意義深いと考える。また、実世界で動作するソフトウェアシステムを（一部の研究ではAIを用いたブラックボックスシステムを）対象とし、その安全性を保証しつつ現実の開発問題に対処する手法を提供している点で社会的にも意義深いと考える。