Authors: URI KLEIN, KEDAR S. NAMJOSHI

Title: Formalization and Automated Verification of RESTful Behavior

Abstract:
REST is a software architectural style used for the design
of highly scalable web applications. Interest in REST has grown rapidly
over the past decade, spurred by the growth of open web APIs. On the
other hand, there is also considerable confusion surrounding REST: many
examples of supposedly RESTful APIs violate key REST constraints. We
show that the constraints of REST and of RESTful HTTP can be pre-
cisely formulated within temporal logic. This leads to methods for model
checking and run-time verfication of RESTful behavior. We formulate
several relevant verification questions and analyze their complexity.