情報処理学会 第78回全国大会講演要旨

モデル検査などを用いたソフトウェアの形式検証についてはそのコストが問題となることが多く、検証過程の初期段階においては検証コストを抑えるため簡素なモデルが利用されている。また、検証用のモデルの作成に関しても、SysMLステートマシン図などの設計情報から検証用モデルを自動生成する技術の研究がなされている。本稿では、検証過程の初期段階で利用可能な簡素なモデルをステートマシン図から自動生成する手法について議論する。特に、検証用モデルとしてモデル検査器SPIN用のモデルについて扱い、ステートマシン図からSPIN用の簡素な検査モデルの変換規則について紹介し、その有効性について議論する。