仕様強化を用いたモデル検査による効率的なブラックボックス検査
Efficient Black-Box Checking via Model Checking with Strengthened Specifications

概要

ブラックボックス検査（Black-box checking）は、ソフトウェアシステムだけでなく、サイバーフィジカルシステム（CPS）にも適用できるテスト手法である。ブラックボックス検査は能動的オートマトン学習とモデル検査から構成され、検査対象システム（System under testing, SUT）から Mealy マシンを学習し、学習した Mealy マシンが仕様を満たしているかモデル検査によって判定する。Mealy マシンが仕様を違反した場合、モデル検査はMealyマシンが仕様を違反している証拠となる入力を返す。この入力を利用して、Mealyマシンの学習を進めるか、SUTが仕様に違反しているとして検査を終了する。Mealyマシンが仕様を違反していなければ、MealyマシンとSUTの違いを示す入力を見つけるために、等価性テストを行う。CPSに対するブラックボックス検査では、システムの実行に時間がかかるため、等価性テストに時間がかかる傾向がある。本研究では、強化された仕様を使ってモデル検査することでブラックボックス検査を効率化する。強化された仕様でモデル検査を行うことにより、元の仕様でモデル検査を行うよりも、仕様を違反している証拠となる入力が得られる可能性が高くなる。このようにして得られた入力を用いてMealyマシンの学習を進めることで，等価性テストの回数を減らすことができ，ブラックボックス検査を効率化できる。本研究では，自動車の変速機のベンチマークを用いて実験を行い、実験の結果から本手法の有効性を示した。

産業界への展開例・適用分野

サイバーフィジカルシステムのブラックボックステスト

研究者

氏名	専攻	研究室	役職/学年
四十坊純也	通信情報システム専攻	五十嵐研究室	修士1回生
和賀正樹	通信情報システム専攻	五十嵐研究室	助教
末永幸平	通信情報システム専攻	五十嵐研究室	准教授