本研究は，今まで進めてきた製品系列に対するファミリーベースモデル検査のスケーラビリティ改善に関する研究を，製品系列以外の単独システムに対しても適用できるように対象範囲を拡大するとともに，機械学習支援と並列処理を採り入れて効率化することで，形式検証の厳密性を担保しつつどこまでスケーラビリティを改善できるかの基本的確認を行うことを目的とする．期間中に以下の研究を進めた．

1.    形式検証に対する機械学習支援の調査：

演繹的かつ論理的な形式手法に対して，機械学習は帰納的かつ統計的な手法であり，双方は対比的性格を持ち相互に補完する研究が進められている．形式検証特にモデル検査技術を対象に，機械学習での支援を行う技術について調査を行い，形式化，検証，ツール実装など広範な検討が進められていることや，各技術の現状での到達度について分かった．今後の研究を進めるための貴重な知見が得られた．

2.    ファミリーベースモデル検査に対する機械学習支援の体系的検討：

形式検証に対して機械学習を適用する手法は数多くあるが，それをアドホックに適用することは適切ではない．そこで今まで進めてきたファミリーベースモデル検査をメタ方法論の手法を用いて整理し，機械学種手法の適用ポイントやその影響などについて体系的に検討を行い，どの部分に機械学習を適用することが有用かなど，今後の研究の方向性を整理した．

3.    機械学習による論理推論の基本的評価：

機械学習手法は形式手法の持つスケーラビリティの課題を改善するひとつの手段として期待されるが，その特性上厳密解を得ることはできない．そこで機械学習が論理推論に対してどのような精度や特性を持つかに関しての基本的な評価を行った．具体的にはSAT問題とモデル検査を対象に基本的な機械学習アルゴリズムを適用し，その精度やそれに影響を与える要因についての評価実験を行い，基本的なデータを得た．