Formal modeling and analysis of the REST architecture using CSP

As one of the most promising architectural styles, Representational State Transfer (REST) was first proposed to support the enablement of scalable and reliable design for largescale distributed hypermedia systems such as the World Wide Web (WWW). Rapidly development of the RESTful systems brings the misunderstanding and misapplied of the REST architecture. In this paper, we present a formal model to capture the essential features for the REST architecture, in which components of RESTful systems are modeled as CSP processes. Thus all the REST constraints can be completely described and validated in our framework. Furthermore, REST constraints are verified using the model checker PAT. The proposed framework for REST architecture is not only confined to HTTP but can also be applied to other REST-compliant protocols. Finally a case study about an application scenario for environment monitoring is illustrated to show the feasibility of our approach. Consequently, better understanding of REST can be achieved and implementations of RESTful systems can benefit from it.