Struts アプリケーションのページ遷移を SPIN を使って検証する話。JSP と Struts 設定ファイルからページ遷移を抽出して promela 記述に落として SPIN へ。ページ遷移のノードは JSP とアクション、遷移は html:form, forward, global-forward などで、いたって普通。

author="Atsuto Kubo and Hironori Washizaki and Yoshiaki Fukazawa",
title="{Automatic Extraction and Verification of Page Transitions in a Web Application}",
booktitle="APSEC 2007",
publisher="IEEE Computer Society Press",
pages="350--357",
year="2007"

JavaCC で生成した解析器で、行にタブ文字がある時に読み取ったトークンの列番号と行頭からのバイト数が合わないと思ったら、列番号が 8 の倍数になるようにタブ文字の幅を決めるようになっていました。これで不思議だった現象は不思議ではなくなったけど、結局オフセットにはどの値を使えばいいのやら。

コメント追加

投稿者 kw : 2008/02/01 17:58:31 JST #