|
組み込みシステムの仕様を記述する際、一度に誤りなく記述するのは困難であるため、誤りのある仕様から修正に有益な情報を得たい。本研究では、誤りのある仕様から、その原因と箇所を表す情報を計算する方法を形式手法により構成した。その計算手法では、仕様を満たす振る舞いを表すωオートマトンにおいてグラフ操作を行なうことで欠陥原因と箇所の情報の計算する。ωオートマトンを簡便に簡約する新しい技術を構成し、解析を効率化しただけでなく、計算する修正情報の形に工夫を加え、現実規模の仕様に適用可能とした。本手法の正当性を証明し、計算量を特定した。さらに、本手法をツールとして実装した。
|
