B-009
形式的仕様記述における制約条件の欠落推定

◎岡野純平・織田　健（電通大）

形式的仕様記述方法の一つ、B-Methodは要求モデルを数学的に記述することで仕様内の無矛盾性を保証することができる。しかし要求モデルが数学的に無矛盾だとしてもそれが利用者の考える振る舞いと一致するとは限らない。その原因の一つとして制約条件の欠落が考えられる。B-Methodでは制約条件によりシステムの無矛盾性を証明するが、制約条件そのものが欠落すると数学的に矛盾が存在しないにも関わらず、利用者の考える振る舞いのソフトウェアを開発できない場合が存在する。本研究の目的は状態遷移図とB-Methodのモデルを比較することで数学的無矛盾性だけでは発見できないモデルの誤りを発見し、その原因と考えられる欠落した制約条件を推測することである。