研究課題
組み込みシステムの仕様を記述する際、センサー等を通じた環境とのやり取りが複雑であり、一度に誤りなく記述するのは困難であるため、誤りのある仕様から修正に有益な情報を得たい。本研究の目的は、誤りのある仕様から、その原因と箇所を表す情報を計算する方法を形式手法により構成することである。平成26年度においては、平成24年度、25年度の成果、即ち、誤り原因を表す情報を計算する方法を実装した。さらに、誤り箇所を表す情報を計算する方法を構成した。本手法の特徴は，実現可能性を直接取り扱わず、代わりにその必要条件である強充足可能性を用いることである．実際の多くの実現不能な仕様は強充足不能であり，解析に必要な計算コストが，実現可能性解析に比べ少ないためである．まず，欠陥箇所を示す概念として極小強充足不能部分を提案し，その導出手続きを構築した．ここで，極小強充足不能部分とは，仕様の強充足不能となる極小部分を示す．提案手続きでは，強充足不能であることを示す反例となる環境からの要求列を入力とし，その実行を表す有向グラフを解析し，その欠陥箇所である極小強充足不能部分を導出する．その手続きの正当性、即ち、健全性、完全性を証明し、手続きの計算量を特定した。さらに、本手法を実装した後、現実的な仕様に適用し、現実時間で欠陥箇所が特定できることを示した。
すべて 2015 2014
すべて 雑誌論文 (4件) (うち査読あり 4件、 オープンアクセス 2件) 学会発表 (9件)
コンピュータソフトウェア
巻: 31(2) ページ: 93-117
10.11309/jssst.31.2_93
IEICE Transactions on Information and Systems
巻: E97-D(7) ページ: 1746-1755
10.1587/transinf.E97.D.1746
巻: 31(3) ページ: 336-356
10.11309/jssst.31.3_336
Communications in Computer and Information Science
巻: 452 ページ: 131-146
10.1007/978-3-662-44485-6_10
