Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bass, L., Clements, P., Kazman, R.: Software Architecture in Practice, 2nd edn. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)
Benslimane, D., Dustdar, S., Sheth, A.P.: Services Mashups: The New Generation of Web Applications. IEEE Internet Computing 12(5), 13–15 (2008)
Berners-Lee, T., Cailliau, R., Groff, J.-F., Pollermann, B.: World-Wide Web: The Information Universe. Electronic Networking: Research, Applications and Policy 1(2), 74–82 (1992)
Blau, B., Lamparter, S., Haak, S.: remash! Blueprints for RESTful Situational Web Applications. In: 2nd Workshop on Mashups, Enterprise Mashups and Lightweight Composition on the Web (MEM 2009) (2009)
Chen, C., Dong, J.S., Sun, J., Martin, A.: A Verification System for Interval-Based Specification Languages. ACM Trans. Softw. Eng. Methodol. 19(4) (2010)
Fielding, R.T.: Architectural Styles and the Design of Network-based Software Architectures (2000)
Garrote, A., Garcia, M.N.M.: RESTful Writable APIs for the Web of Linked Data Using relational Storage Solutions (April 2011)
Hernández, A.G., GarcÃa, M.N.M.: A Formal Definition of RESTful Semantic Web Services. In: WS-REST, pp. 39–45 (2010)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
Klein, U., Namjoshi, K.S.: Formalization and Automated Verification of RESTful Behavior. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 541–556. Springer, Heidelberg (2011)
Koch, N.: Reference Model, Modeling Techniques and Development Process Software Engineering for Adaptive Hypermedia Systems. KI 16(3), 40–41 (2002)
Luu, A.T., Sun, J., Liu, Y., Dong, J.S., Li, X., Tho, Q.T.: SeVe: Automatic Tool for Verification of Security Protocols. Frontiers of Computer Science in China 6(1), 57–75 (2012)
Pautasso, C.: RESTful Web service composition with BPEL for REST. Data Knowl. Eng. 68(9), 851–866 (2009)
Pautasso, C., Zimmermann, O., Leymann, F.: REST vs. SOAP: Making the Right Architectural Decision (Jul 2008)
Roscoe, A.: Understanding Concurrent Systems. Springer (2010)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1998)
Sun, J., Liu, Y., Dong, J.S.: Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. In: ISoLA 2008. CCIS, vol. 17, pp. 307–322. Springer, Heidelberg (2008)
Taylor, R.N., Medvidovic, N., Anderson, K.M., Whitehead Jr., E.J., Robbins, J.E., Nies, K.A., Oreizy, P., Dubrow, D.L.: A Component- and Message-Based Architectural Style for GUI Software. IEEE Trans. Softw. Eng. 22(6), 390–406 (1996)
Wu, X., Liu, S., Zhu, H., Zhao, Y., Chen, L.: Modeling and Verifying the Ariadne Protocol Using CSP. In: ECBS, pp. 24–32 (2012)
Yeung, W.L.: CSP-Based Verification for Web Service Orchestration and Choreography. Simulation 83(1), 65–74 (2007)
Zuzak, I., Budiselic, I., Delac, G.: Formal Modeling of RESTful Systems Using Finite-State Machines. In: Auer, S., DÃaz, O., Papadopoulos, G.A. (eds.) ICWE 2011. LNCS, vol. 6757, pp. 346–360. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wu, X., Zhang, Y., Zhu, H., Zhao, Y., Sun, Z., Liu, P. (2013). Formal Modeling and Analysis of the REST Architecture Using CSP. In: ter Beek, M.H., Lohmann, N. (eds) Web Services and Formal Methods. WS-FM 2012. Lecture Notes in Computer Science, vol 7843. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38230-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-38230-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38229-1
Online ISBN: 978-3-642-38230-7
eBook Packages: Computer ScienceComputer Science (R0)