Formalization And Verification Of REST And SA-REST In Viewpoints

Representational State Transfer (REST), as a promising software architecture style, has been used in large scale since proposed. However, there still exist considerable confusions about the REST architecture, which may lead to inappropriate application. We apply formal method CSP in modeling the REST architectural style to give a comprehensive explanation of it. The architectural description is partitioned into three separate views:process view, connector view and data view, each capturing one architectural element and related properties of the architecture. Furthermore, REST constraints can be described in our framework and validated by the model checker PAT. Besides, we focus on the relation between the stateless constraint and application state, resource state, as well as the uniform interface constraint and hypermedia-driven property. The related properties of them are also verified in this paper.The Semantic Web is an extension of the Web through standards by the World Wide Web Consortium. The standards promote common data formats and exchange protocols on the Web, most fundamentally the Resource Description Framework (RDF). Semantic Annotation of Web Resources (SA-REST) is a poshformat to add additional meta-data to REST API descriptions in HTML or XHTML. This embedded meta-data permits various enhancements, such as improve search, facilitate data mediation and easier integration of services. The use of SA-REST enabled services for creating dynamic mashups called SMashups. We apply formal method CSP and PAT in modeling and verification of SMashup to analyze the properties about service chain, grounding schema and ontology.