|
組込みソフトウェアの検証・試験フェーズ（以降では検証というときはモデルを対象とし、試験というときにはプログラムが対象であるとする）では、つぎのことが課題として取り上げられている。
・試験時間に関する課題
・検証・試験の質に関する課題
最初に試験時間に関する課題とは、限られた開発期間の中で検証や試験に充当できる時間が限られており満足のいくレベルまで検証・試験が出来ないというものである。つぎの検証・試験の質に関する課題とは、検証・試験の質が担当者の経験に依存した方式に陥りがちで検証・試験の質にばらつきが生じてしまうということである。前者は、近年組込みソフトウェアも規模が増大しているにもかかわらず開発期間が十分に取れないことに原因がある。また、後者の原因としてつぎのことが考えられる。検証・試験を効率的に実施するためのツールが十分に整備されていないために生じる。
モデル検証ツールとして SPIN, FDR がすでに知られている。これらは、モデルの検査を行うためのツールである（以下、モデル検証ツールという）。形式的にシステムのモデルの正当性を示すものである。しかし、モデルの実体であるプログラムを試験することはできない。これまでのモデル検証ツールはモデルの検証を行うだけである。
我々は、モデル検証ツールをプログラム試験にまで利用できるテスティングツールを開発する。これにより、試験時間の短縮と試験の質の向上に寄与する。モデル検証において作成したモデルをもちいてプログラム試験を行うことにより試験時間を短縮し、形式的手法をもちいることで試験の質を向上させる。
|
