Formalization and verification of REST on HTTP using CSP

Representational State Transfer (REST), as a promising software architecture style, has been used in large scale since proposed. But considerable confusions about REST exist and many examples of supposedly RESTful applications violate key REST constraints. In this paper, we focus on the most important constraints of REST, stateless property and hypertext-driven property. First we establish a formal model for REST on HTTP in CSP. In the model, components in RESTful systems communicate with each other using standard HTTP methods and are modeled as CSP processes. From the model we can find the effects of HTTP methods on resources. Then we give formal descriptions for failure cases of stateless, hypertext-driven constraints of REST, and safe, idempotent properties of HTTP methods, within which whether a system breaks REST constraints or basic HTTP requirements can be checked. Furthermore, we use model checker PAT to prove all the constraints hold in our model. In the end, a case study about the process of buying food is mapped to our model to better illustrate the REST concepts and our approach.