Formalization and analysis of the REST architecture from the process algebra perspective

As one of the most promising architectural styles, REpresentational State Transfer (REST) was proposed to support a scalable and reliable design for large-scale distributed hypermedia systems such as the World Wide Web (WWW). However, the rapid development of RESTful systems brings the misunderstanding and misapplying of the REST architecture. As a consequence, considerable confusions about REST exist and many examples of supposedly RESTful applications violate key REST constraints. Thus, it is of significant importance to give a better and explicit understanding of REST architecture to guide the design and implementations of RESTful systems.In this paper, we give a formalization and analysis of the REST architecture from the perspective of Communicating Sequential Processes (CSP), which is one of the most famous process algebras. In particular, we present a formal model to capture essential features for the REST architecture, where components (together with one connector) of RESTful systems are modeled as CSP processes. Besides, resources are also abstracted as CSP processes. Furthermore, all the REST constraints, including Client–Server, Cacheable, Stateless, Uniform Interface, Layered and Code-On-Demand, are described in our framework and implemented in the model checker Process Analysis Toolkit (PAT) to check whether a system breaks REST constraints or not. It is difficult to ensure that a system is RESTful system, because many unRESTful systems may also contain unRESTful properties besides satisfying the six REST constraints. Thus, a complementary approach is proposed in this paper to check the system from a different perspective; that is, if a system breaks any specification of the REST constraints, then it is not a RESTful system. Finally, to show the feasibility of our approach, we illustrate a case study about an application scenario for environment monitoring. One feature of the proposed framework for the REST architecture is that it not only confines to HyperText Transport Protocol (HTTP) but can also be applied to other REST-compliant protocols, e.g., Constrained Application Protocol (CoAP). Consequently, through the general framework, a better understanding of the REST architecture can be achieved, and moreover, implementations and designs of RESTful systems can benefit from it.