| 研究課題/領域番号 |
17H01727
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
石川 冬樹 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (50455193)
|
|---|
| 研究分担者 |
本位田 真一 早稲田大学, 理工学術院, 教授(任期付) (70332153)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
14,300千円 (直接経費: 11,000千円、間接経費: 3,300千円)
2020年度: 5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
2019年度: 2,990千円 (直接経費: 2,300千円、間接経費: 690千円)
2018年度: 2,990千円 (直接経費: 2,300千円、間接経費: 690千円)
2017年度: 3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
|
|---|
| キーワード | ソフトウェア開発効率化・安定化 / 形式手法 / システムモデリング / 段階的詳細化 / Cyber-Physical Systems / ソフトウエア開発効率化・安定化 |
|---|
| 研究成果の概要 |
実世界・社会に踏み込むソフトウェアシステムにおいては，その仕様と想定環境のかみ合わせにより要求が満たされることの検証が重要かつ困難な課題である．これに対し多段階の抽象度からなるモデルを用い，複雑さを軽減しつつシステムモデルの記述と検証を行うアプローチが注目されている．しかし整合性検証に適した多段階モデルを設計し，また検証済みの整合性を壊さず継続的に変更していくことは難しい．これに対し本研究では，断片的な記述を逐次的に与えて多段階モデルを洗練させていく手法に取り組んだ．また自律制御システムにおける先端的な題材に対し提案手法を適用しその有効性を確認した．
|
| 研究成果の学術的意義や社会的意義 |
多数の構成要素を含むソフトウェアシステム全体について安全性を一括で論じることは困難です．このため，単純な場合からはじめて，システムをとらえる抽象度（解像度）を少しずつ上げながら，安全性を論じていく方法があります．しかし，「単純な場合ではよかったが，この要素が入ると安全性保証がやり直しになる」ことが起きてしまいます．本研究では，「既存の安全性保証を壊さずに追加要素を加える」という技術を軸に，段階的に安全性の保証を論じる方法論を確立しました．これにより，ますます複雑になるソフトウェアシステムに対し，強力な安全性保証をより容易に行うことができるようになりました．
|
