2014 Fiscal Year Annual Research Report
形式手法による欠陥のある現実規模の組み込みシステム仕様からの修正情報抽出
| Project/Area Number |
24500032
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
萩原 茂樹 東京工業大学, 情報理工学(系)研究科, 助教 (70334547)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 形式手法 / 組み込みシステム仕様 / 修正情報抽出 |
|---|
| Outline of Annual Research Achievements |
組み込みシステムの仕様を記述する際、センサー等を通じた環境とのやり取りが複雑であり、一度に誤りなく記述するのは困難であるため、誤りのある仕様から修正に有益な情報を得たい。本研究の目的は、誤りのある仕様から、その原因と箇所を表す情報を計算する方法を形式手法により構成することである。平成26年度においては、平成24年度、25年度の成果、即ち、誤り原因を表す情報を計算する方法を実装した。さらに、誤り箇所を表す情報を計算する方法を構成した。本手法の特徴は，実現可能性を直接取り扱わず、代わりにその必要条件である強充足可能性を用いることである．実際の多くの実現不能な仕様は強充足不能であり，解析に必要な計算コストが，実現可能性解析に比べ少ないためである．まず，欠陥箇所を示す概念として極小強充足不能部分を提案し，その導出手続きを構築した．ここで，極小強充足不能部分とは，仕様の強充足不能となる極小部分を示す．提案手続きでは，強充足不能であることを示す反例となる環境からの要求列を入力とし，その実行を表す有向グラフを解析し，その欠陥箇所である極小強充足不能部分を導出する．その手続きの正当性、即ち、健全性、完全性を証明し、手続きの計算量を特定した。さらに、本手法を実装した後、現実的な仕様に適用し、現実時間で欠陥箇所が特定できることを示した。
|
Research Products
(13 results)
