非同期通信を行うWebアプリケーションによる資源競合問題に対するモ デル検査による検証

摘要

Client-side usability become more and more important to develop the Web aplication. For example, Ajax allows sending requests asynchronously without blocking clients. However, server processing is performed in order not anticipated by the asynchronous communication. In this paper, we demonstrate the possible problems caused by the asynchronism and how to solve aproblem. It has been considered model checking can be used to solve this problem. But expertise and effort is a challenge. In this paper, we propose a method for validation that can also be used for general engineer. It is necessary only to describe the order of acquisition and release of resources. So It can reduce the efforts and be eliminating the need for expertise mitigation.%Webアプリケーションの開発においては，クライアント側のユーザビリティ向上が重要になってきている。たとえばAjaxなどの技術における非同期通信の利用により，クライアント側の操作をブロックせずに動作することが可能となっている.しかしながら，非同期通信によって予期しない順序でサーバ処理が行われる可能性がある.本研究では，特に資源へのアクセスと非同期通信の使用時に起こる可能性のある問題と解決方法を示す.従来はこのような問題に対し，モデル検査などの形式検証手法が有効であると考えられてきたが，専門知識が必要でかつ検証の労力が大きいという課題があった.本論文では，モデル検査による検証手法を，一般の技術者にも容易に利用可能とするための検証手法を提案する.これにより開発者は資源競合の検証において，Webアプリケーションのモデルを記述せず，資源へのアクセスの順序を記述するだけで良くなるので，専門知識が不要となり，かつ検証時の労力の大幅な軽減が可能となった.