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

近年，組込みソフトウェアの開発にUMLが広く用いられるようになってきている．UMLはソフトウェアの全体像の把握を容易にする一方で，書いたモデルの厳密な検証を前提にしておらず，モデルの正しさを示すことが困難である．さらに頻繁に更新され続ける各図間のトレーサビリティーを保ち続けることは大きな負担になる．そこで，離散数学を基盤にした検証でソフトウェアの信頼性を向上させる形式手法とUMLモデルを組み合わせ，UMLモデルの厳密な検証を可能にする研究が進められている．そこで本研究では，モデル検査手法を用いることにより，UMLモデルの厳密な検証を可能にし，複数モデル間でのトレーサビリティーを論理的に示す方法を検討する．