5H-09
状態遷移図と抽象的仕様記述のマッチングによる仕様の誤り検出
○岡野純平（電通大）
近年ソフトウェア開発では信頼性が求められる。B-methodは仕様を集合論に基づいた
記述を行うことで仕様の無矛盾性を証明によって検証することができ、開発された
ソフトウェアの信頼性を確保できる。
しかしB-methodには制約条件の欠落を原因とした誤りが存在する場合がある。
この場合、記述された仕様は、検証によって仕様内に矛盾が存在しないと評価される
にも関わらず、この仕様を基に開発されたソフトウェアの振る舞いが
利用者の要求と異なる可能性がある。
そこで、本研究ではB-methodと状態遷移図の2つの記法で仕様を記述し、
その2つを比較することで仕様の誤りを検証する手法を提案する
footer 著作権について 倫理綱領 プライバシーポリシー セキュリティ 情報処理学会