Model Checking Based Conformance Testing for Web Applications

Usually, conformance testing is done in a way that testers having a running application and its specification, test whether the implementation of the application conforms to its specification. Only when deploying the web application on the server, users can access it through the client software called web browsers. The features of web browsers influence the functionalities of web applications. So, even if we can ensure that the implementation of the web application conforms to its specification, still there is no guarantee that the specification conforms to its implementation. This paper proposes a model checking based approach to automatically executing conformance testing of web applications and can ensure that the implementation conforms to its specification and the specification conforms to its implementation, respectively. The implementation models are abstracted from the running web applications As for unsatisfied CTL formulas, according to the counterexamples, we can locate the uncomformance in implementation or in specification.