We propose a method for modelling navigation structure of web application using state machine diagrams. We assume that the navigation structure is described by a page flow diagram. The navigation structure is modelled as state machine diagrams representing page navigations, authentication and user operations. A model of page navigations is obtained by representing web pages and movement of them as states and transitions, and by representing form controls in web pages as substates. A model of authentication is obtained by representing a condition of authorization as states which changes by events corresponding to user operations. User operations are represented as actions in transitions. We applied the proposed method to an example web application described by a page flow diagram and modelled it as state machine diagrams. We demonstrated automatic verification and test generation for the obtained state machine diagrams using SAL tools. We showed that errors in the page flow diagram can be detected successfully and the generated test case can cover all navigations. Additionally, we applied the method to a practical example and showed that verification and test generation by SAL can be carried out in a small amount of time.
