|
当初の研究計画で挙げていたネットワーク検証に向けた応用研究の取り組みとして、有界モデル検査のエラー解析手法を開発した（Interval-based Counterexample Analysis for Error Explanation）。有界モデル検査は、ハードウェアやソフトウェアに含まれる設計ミスを検出するための実用的な手法である。もし検査対象のシステムに仕様違反が存在するならば、有界モデル検査は仕様に違反するシステムの動作例（仕様に対する反例）を出力する。
有界モデル検査により反例の計算までは自動化されるが、反例からシステムの設計ミスの場所を特定する作業は通常人手で行われている。
本研究では、この作業を支援することを意図して、通常の反例よりも高い抽象度で設計ミスの原因を説明する手法を与えた。本手法の中では、AllSAT問題を解くソルバーとその出力結果を効率的に表現するデータ表現（BDD）を組合せて、処理の効率化を実現している。命題論理式の解を１つ求めることは一般にNP完全であるが、AllSATはすべての解を計算することが求められ、非常に困難な計算となる。実際の応用では必ずしもすべての解までは必要なく、むしろ多様性のある（比較的少数の）解を求めることで十分な場合も多い。そこで、本研究課題では解のサンプリングに関する研究にも取り組んだ。まず、従来のサンプリング手法の精度を向上させるための技術を開発した（命題論理式の解の一様サンプリングの改善）。さらに、サンプリング手法を活用した応用研究として、複合イベント処理システムを開発した（不確実性下における複合イベント処理に関する考察）。
また、その他の展開として、データベースの匿名化手法に関する研究にも取り組み、既存の枠組みを拡張する新しい手法を開発した（属性間依存度を考慮したデータベースの安全なフラグメント化）。
|
