ソフトウェアを設計・実現したときに， それらがもともとの要求に対して，正しいということをなんらかの方法で 確かめておく必要があります． 例えば， 電子商業取引を行うためのソフトウェアや交通制御システムなどの重要性を考えれば， それらの設計や実現の正しさをできるだけ確認しておくことの重要性は 明らかでしょう．

ところで， それらが正しいということを確認するには， 多くのテストを行うなど，いくつか方法が考えられますが， 実際には， どの方法を用いても完全に正しさを 確認できたと言えないのが現状です．この研究では， 少しでも，その正しさの確認をより完全なものに近づけるために 以下のようなアプローチを研究しています．

それは，作成された設計・実現に対してそれが正しいという条件を表す論理式をつくり, その式が本当に成り立つかを調べるという方法です（論理式が成り立てば, その設計・ 実現が正しいということが数学的に成り立ちます）．この際, そのような論理式は非常に膨大かつ複雑になるので， そのような式の生成や成立するかどうかの検査にコンピュータを使うことにな ります．

∀x∃y{(x≤0 ∧ y> 0) ∨ (y=0 ∧ x≠ y) → y>0}

これらの作業は，たとえば，自動車を実際につくる前に， 設計図を作成し，そこから， 強度計算， 走行性能計算などをするために， 複雑な方程式を作成し，その方程式を解くという作業になぞらえることができます． 対象が，ソフトウェアであることによる大きな違いは， そのような方程式の作成や，解法のうち多くの作業をコンピュータで自動化 できるという点です．

論理式を調べる技術については最近ではモデル検査技術の研究が進みその恩恵を得ることができるようになってきています．

しかしながら，モデル検査技術を使うにしても調べたい性質の導出や調べたい対象のモデル化（形式化）についてはまだまだ研究の余地がのこっています．

最近は，機械学習の研究の発展にともない，機械学習を応用した要求仕様書の解析や状態遷移モデル，検証性質への自動変換を精力的に行っています．さらにその発展として機械学習を持田要求仕様の自動分類、プログラムコードのバグ解析、あるいは、機械学習データや機械学習アルゴリズムの品質の評価などの研究も始めています．

最新のテーマ

岡野の研究室ではモデル検査技術、SAT/SMTソルバーなどの最新の技術を使って高品質ソフトウェア開発の支援をする技術の研究を行っています。最近は機械学習の研究の発展にともない、機械学習を応用したソフトウェア開発として要求仕様書の解析やプログラムコードのバグ解析、あるいは、機械学習データや機械学習アルゴリズムの品質の評価などの研究を始めています。これらの研究は複数の研究機関の研究者と共同研究の形で実施しています。

具体的には以下のようなテーマについて研究を行なっています

• 機械学習を用いたプログラムのバグ解析

• モデル指標にもとづく機械学習アルゴリズムの欠陥発見

• モデル指標にもとづく機械学習データの品質判定

• 要求仕様書の自然語解析による分類、バグ発見

• STAMP/STPAへのフォーマルアプローチの適用