形式的手法によるWebアプリケーションのモデル化と検証

摘要

オンライントランザクションを扱うWebアプリケーションの数は年々増加している．しかし，Webアプリケーションの設計に対する正常稼働の確認は人手で行っているのが現状である．本稿では，Webアプリケーションの設計で利用される画面遷移図とアプリケーション内部の状態を2つの有限状態オートマトンとして，Webアプリケーションをモデル化する手法を提案する．また，モデル化した設計を用いて形式的手法によるモデル検査を実施したのでその事例を合わせて報告する．