Formal verification of web applications modeled by communicating automata

In this paper, we present an approach for modeling an existing web application using communicating finite automata model based on the userdefined properties to be validated. We elaborate a method for automatic generation of such a model from a recorded browsing session. The obtained model could then be used to verify properties with a model checker, as well as for regression testing and documentation. Unlike previous attempts, our approach is oriented towards complex multi-window/frame applications. We present an implementation of the approach that uses the model checker Spin and provide an example.