2019 Fiscal Year Annual Research Report
Continuous and Flexible Sophistication and Evolution of Assured Multi-Level System Models
| Project/Area Number |
17H01727
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
石川 冬樹 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (50455193)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
本位田 真一 早稲田大学, 理工学術院, 教授(任期付) (70332153)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | ソフトウェア開発効率化・安定化 / 形式手法 / システムモデリング / 段階的詳細化 / Cyber-Physical Systems |
|---|
| Outline of Annual Research Achievements |
実世界・社会に踏み込むソフトウェアシステムに置いては，その仕様と想定環境のかみ合わせにより要求が満たされることの検証が重要かつ困難な課題である．これに対し多段階の抽象度からなるモデルを用い，複雑さを軽減しつつシステムモデルの記述と検証を行うアプローチが注目されている．しかし整合性検証に適した多段階モデルを設計し，また検証済みの整合性を壊さず継続的に変更していくことは難しい．これに対し本研究では，断片的な記述を逐次的に与えて多段階モデルを洗練させていくと共に，実行時の監視データとの照らし合わせも通してさらに多段階モデルを適合させていくための枠組みを構築する．この枠組みは具体的には形式手法Event-B上にて実現する．
２０１９年度においては，鉄道や自律制御システムなどにおける先端的な題材を構築しつつ，これまで構築した技術の一般化や統合に取り組んだ．Event-B手法における記述の誤りや漏れのパターン，および変更のパターンを整備することで，変更による影響の把握や，それを防ぐように制約された変更が行えるようになった．またソフトウェアテスト分野におけるミューテーション分析とのアナロジーを考えることで，システム制約の記述不足の検出など新たな展開も行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
ミューテーション分析とのアナロジーによる不変条件修正など新たな方向性での取り組みに広がっている．
|
| Strategy for Future Research Activity |
これまでの取り組みにおいて，新しい応用事例を産学連携により得ることができたため，その事例での価値も重視し，これまでの成果をまとめ活用できるようにしていく．
|
