Formalization And Analysis Of RESTful Web Service

As Web service has been used in large scale over the last decade, more and more researchers and developers show interests in the fields related to REST architectural style. REST architecture has simplicity, scalability, flexibility, reusability and low coupling and it gains great momentum. RESTful Web service is a resource-oriented web service that conforms to REST architectural style, using URI as its uniform resource identifier and HTTP methods as its uniform methods. REST architectural style has little research in terms of formal methods since proposed. And as a result, considerable confusions about its design principles exist and examples of supposedly RESTful applications violate key REST constraints.We establish a formal model for RESTful Web service in CSP and also analyze its most important constraints in this thesis. First, two formal models are given, one is for REST architecture and the other is for RESTful Web service. The first model focuses on the detailed structure of each component while the second model describes the interactions between the components. We have three components in our second model:client, server and resource. Each of them is modeled as a CSP process and communicates with each other using standard HTTP methods. From the model we can find the effects of HTTP methods on resource since resource itself is described as a process. We also give formal descriptions for stateless, hypertext- driven constraints of REST, and safe, idempotent properties of HTTP methods. Furthermore, we use model checker PAT to prove all the constraints hold in our model. In the end, a case study is mapped to our model to illustrate the REST concepts and our approach.The formalization and verification of RESTful Web service helps in better understanding of the REST concepts. And the descriptions of the constraints can help to check whether a system breaks REST constraints or basic HTTP requirements.