Formal Models for Web Navigations with Session Control and Browser Cache

While providing better performance, transparency and expressiveness, the main features of the web technologies such as web caching, session and cookies, dynamically generated web pages etc. may also affect the correct understanding of the web applications running on top of them. From the viewpoint of formal verification and specification-based testing, this suggests that the formal models of the web applications we use for static analysis or test case generation should subsume the abstract behavior of their supporting environment. Here we provide the definition of such a model in terms of labelled transition systems from a given abstract description of the navigations of a web application by incorporating the abstract behavioral model of the web browsers in the presence of session control and browser cache. The significance of the work is twofold: on one hand, it provides a formal basis for better understanding of the web systems; on the other hand, it lays the ground work for both model checking and specification-based testing on the web applications where we take into account the affect of the internal mechanism to the correct web navigations, which can be quite sensitive to the security of the information they carry.