Formalization and Automated Verification of RESTful Behavior

REST (REpresentational State Transfer) is a software architectural style used in the design of highly scalable web services. Interest in REST has grown rapidly over the past decade, arising from efforts to provide open APIs for web services. On the other hand, there is also considerable confusion about REST, exemplified by well-known APIs that are claimed to be RESTful, but which violate one or more of the principles of REST. Thus, REST is an especially good subject for formal modeling. In this paper, we show that the defining principles of REST, and of RESTful HTTP systems in particular, can be precisely formulated in temporal logic. We define several automated verification questions and discuss their complexity. These include model-checking for RESTfulness, and the use of run-time monitors to detect violations.