システム検証の一種であるプロパティ検証と呼ばれる、システムが仕様(プロパティ)を満たすかどうかを確かめる検証方法を対象として、検証がどの程度網羅的に行われているかを示す指標となる検証カバレッジを提案し、その評価を行った。検証においては、システム全体のうち、どの程度の部分が検証できているかを知ることが重要であるが、プロパティ検証ではそのような指標が存在しないため、指標の確立は重要である。本研究では、システムの状態遷移が変化することによって、検証結果がその影響によって変化した場合、検証したプロパティによってその状態遷移が網羅されていると考え、これに基づく検証カバレッジを提案し、評価結果を示した。
|