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

2019 Fiscal Year Research-status Report

• Project/Area Number: 19K20249
• Research Institution: National Institute of Informatics
• Principal Investigator: 小林 努 国立情報学研究所, コンテンツ科学研究系, 特任研究員 (10803405)
• Project Period (FY): 2019-04-01 – 2022-03-31
• Keywords: ソフトウェア / 形式手法 / システムモデリング / 段階的詳細化 / Event-B

Outline of Annual Research Achievements

変化する複雑な環境の中で動作する、高い安全性が求められるソフトウェアの需要が増加している。これに対し、動作環境と制御器の動作を形式的な仕様で記述して検証するアプローチが有効だが、現実の環境には開発時の想定と違う振る舞いや変化が存在する。
そこで、本研究では、環境が変化した際に、要求を満たすように整合性のある形で制御器を適切に変更(適応)することで、実世界で動くソフトウェアの安全性向上に寄与することを目指している。
2019年度においては、形式仕様記述手法Event-Bの仕様を対象とし、環境の変化のしかたに応じて、制御器のどの部分をどのように変更する必要があるかについてのパターンの構築に取り組んだ。これにより、提案全体の基礎部分を構築でき、パターンに従うことで(手動で)体系的に適応操作を行えるようになった。また、要求を満たすような適応がそもそも可能かどうかの判断の手掛かりも得られるようになった。この成果は、来年度以降の研究の基礎ともなる。

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

2019年度の実施を計画していたように、適応パターンを構築することができた。
要求を満たす適応が可能かどうかの判断手法については発展の余地はあるものの、基礎を構築できた。

Strategy for Future Research Activity

今後は、2019年度の成果をもとに、制御器をどこまで変更できるかの分析や、多段階の抽象度を持つ形式仕様に対する適応手法の構築を行う。

Causes of Carryover

海外の形式仕様記述手法の専門家と本研究に関する共同研究のための諸費用を計上していたが、議論の結果、特に今後実施予定の多段階抽象度にわたる形式仕様の適応に関して集中的に共同で取り組むことになった。
そのため、次年度に当該額を使用する。