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

本研究では，リッチクライアントのようなページ内遷移するWebアプリケーションを対象とした検証手法を提案し，その有効性を示す．
リッチクライアントにはイベントハンドラが使用されている．複数のイベントハンドラが競合した場合，Webアプリケーションが予期しない動作を起こす事例がある．
一般にWebアプリケーションの動作検証にはモデル検査法が用いられている．
本研究では，イベントハンドラの動作仕様を状態遷移図で表し，その状態遷移図のXML文書を構文解析すること仕様記述言語Promelaコードを自動的に出力する．
そして，検査項目は時相論理式を用いて定義する．本研究で提案した手法を適用することにより，テストでは発見が困難であるエラーを検出し，その手法の有効性を示した．