| 研究課題/領域番号 |
17H01727
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
石川 冬樹 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (50455193)
|
|---|
| 研究分担者 |
本位田 真一 早稲田大学, 理工学術院, 教授(任期付) (70332153)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | ソフトウエア開発効率化・安定化 / 形式手法 / システムモデリング / 段階的詳細化 / Cyber-Physical Systems |
|---|
| 研究実績の概要 |
実世界・社会に踏み込むソフトウェアシステムにおいては，その仕様と想定環境のかみ合わせにより要求が満たされることの検証が重要かつ困難な課題である．これに対し多段階の抽象度からなるモデルを用い，複雑さを軽減しつつシステムモデルの記述と検証を行うアプローチが注目されている．しかし整合性検証に適した多段階モデルを設計し，また検証済みの整合性を壊さず継続的に変更していくことは難しい．これに対し本研究では，断片的な記述を逐次的に与えて多段階モデルを洗練させていくとともに，実行時の監視データとの照らし合わせも通してさらに多段階モデルを適合させていくための枠組みを構築する．この枠組みは形式手法Event-B上にて具体的なツールとして実現する．
平成３０年度においては，多段階モデルにおいて整合性を壊さず段階構造を柔軟に再構成するための技術について，ツール化および様々な構成設計を評価する実験に取り組んだ．これにより，本研究の基礎となる技術を確立しつつ，その技術により従来行われていなかった斬新な実験を行うことができた．次に，これまで扱ってきたものよりも細粒度の変更に対する影響分析の手法も確立した．これにより，本研究により支援する変更の範囲を拡げることができた．加えて，計画時には想定していなかった成果として，連続的変化を含むサイバーフィジカルシステムを扱うためのEvent-Bの拡張を考慮するような追加の取り組みも行った．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
計画時には想定していなかった成果として，連続的変化を含むサイバーフィジカルシステムを扱うためのEvent-Bの拡張を考慮するような追加の取り組みも行った．
|
| 今後の研究の推進方策 |
引き続き，反復的に具体的な利用シナリオに基づきながら，研究を進める．計画時には想定していなかった物理的挙動の扱いについても，自動運転などの例題を基に注力して進める．
|
