UMLモデルからの変換によるWebアプリケーションの形式検証

摘要

モデル検査法がアプリケーションソフトウェアの形式検証のために適用されつつある．ソフトウェア開発の上流工程ではモデルを開発成果物とすることが多く，その成果物としてUMLが普及している．UMLのモデルを形式検証に活用するために，モデルから検証可能なオートマトンへと変換する手法が提案されている．我々は，WebアプリケーションのUMLモデルを，検証可能なオートマトンへ変換する手法を提案する．従来手法では，オートマトン生成のための情報をモデルに付加していたが，本手法ではWebアプリケーションモデリング以外の情報をモデルの前提としない．モデリング対象は携帯電話向けのWebアプリケーションとし，検証条件はセッションに関するセキュリティ脆弱性の不存在とした．