Model checking class specifications for Web applications

This paper proposes an approach for verifying class specifications of Web applications using model checking. We first present a method to model a dynamic behavior of a Web application from a class specification. We next propose two methods to verify consistencies of the class specification and other design specifications: (1) a page flow diagram which is one of the most essential specifications for Web applications and (2) a behavior diagram such as a UML activity diagram. We applied the proposed methods to real specifications of a Web application designed by a certain company and found several faults of the specifications that had not been detected in actual reviews.