Abstract
Web services are highly distributed programs and, thus, are prone to concurrency-related errors. Model checking is a powerful technique to identify flaws in concurrent systems. However, the existing model checkers have only very limited support for the programming languages and communication mechanisms used by typical implementations of web services. This chapter presents a formalization of communication semantics geared for web services, and an automated way to extract formal models from programs implementing web services for automatic formal analysis. The formal models are analyzed by means of a symbolic model checker that implements automatic abstraction refinement. Our implementation takes one or more PHP5 programs as input, and is able to verify joint properties of these programs running concurrently.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Douglas K. Barry. Web services and service-oriented architectures. Morgan Kaufmann, 2003.
Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, December 1999.
Edmund M. Clarke and E. Allen Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, volume 131 of Lecture Notes in Computer Science. Springer, 1981.
Jerry R. Burch, Edmund M.Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
Gerard J. Holzmann and Doron Peled. An improvement in formal verification. In Dieter Hogrefe and Stefan Leue, editors, Formal Description Techniques VII, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques, Berne, Switzerland, 1994, volume 6 of IFIP Conference Proceedings, pages 197–211. Chapman & Hall, 1995.
Patrik Cousot. Abstract interpretation. Symposium on Models of Programming Languages and Computation, ACM Computing Surveys, 28(2):324–328, June 1996.
Susanne Graf and Hassen Saïdi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Proc. 9th International Conference on Computer Aided Verification (CAV’97), volume 1254, pages 72–83. Springer, 1997.
Michael Colón and Thomás E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In Computer Aided Verification (CAV), volume 1427 of Lecture Notes in Computer Science, pages 293–304. Springer, 1998.
Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. In POPL, 1992.
Thomas Ball and Sriram K. Rajamani. Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research, February 2000.
Thomas Ball, Rupak Majumdar, Todd D. Millstein, and Sriram K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation, pages 203–213. ACM, 2001.
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, and Helmut Veith. Modular verification of software components in C. In ICSE, pages 385–395. IEEE Computer Society, 2003.
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Software verification with BLAST. In Thomas Ball and Sriram K. Rajamani, editors, SPIN, volume 2648 of Lecture Notes in Computer Science, pages 235–239. Springer, 2003.
Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, and Karen Yorav. SATABS: SAT-based predicated abstraction for ANSI-C. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 570–574. Springer, 2005.
PHP: Hypertext preprocessor. http://www.php.net/.
http://www.asp.net/.
http://www.ibm.com/developerworks/library/specification/ws-bpel/.
Bernd-Holger Schlingloff, Axel Martens, and Karsten Schmidt. Modeling and model checking web services. Electr. Notes Theor. Comput. Sci., 126:3–26, 2005.
Raman Kazhamiakin, Marco Pistore, and Luca Santuari. Analysis of communication models in web service compositions. In WWW ’06: Proceedings of the 15th international conference on World Wide Web, pages 267–276, New York, NY, USA, 2006. ACM Press.
Marco Pistore, Paolo Traverso, Piergiorgio Bertoli, and Annapaola Marconi. Automated synthesis of executable web service compositions from BPEL4WS processes. In Ellis and Hagino DBLP:conf/www/2005si, pages 1186–1187.
Allan Ellis and Tatsuya Hagino, editors. Proceedings of the 14 th international conference on World Wide Web, WWW 2005, Chiba, Japan, May 10-14, 2005 - Special interest tracks and posters. ACM, 2005.
Tuba Yavuz-Kahveci, Constantinos Bartzis, and Tevfik Bultan. Action language verifier, extended. In Kousha Etessami and Sriram K. Rajamani, editors, CAV, volume 3576 of Lecture Notes in Computer Science, pages 413–417. Springer, 2005.
Xiang Fu, Tevfik Bultan, and Jianwen Su. Analysis of interacting BPEL web services. In Stuart I. Feldman, Mike Uretsky, Marc Najork, and Craig E. Wills, editors, WWW, pages 621–630. ACM, 2004.
Xiang Fu, Tevfik Bultan, and Jianwen Su. Model checking XML manipulating software. In George S. Avrunin and Gregg Rothermel, editors, ISSTA, pages 252–262. ACM, 2004.
Tevfik Bultan, Xiang Fu, Richard Hull, and Jianwen Su. Conversation specification: a new approach to design and analysis of e-service composition. In WWW, pages 403–410, 2003.
Daniel Kroening and Natasha Sharygina. Formal verification of SystemC by automatic hardware/software partitioning. In Proceedings of MEMOCODE 2005, pages 101–110. IEEE, 2005.
Shin Nakajima. Model-checking of safety and security aspects in web service flows. In Nora Koch, Piero Fraternali, and Martin Wirsing, editors, Web Engineering - 4th International Conference, ICWE 2004, Munich, Germany, July 26-30, 2004, Proceedings, volume 3140 of Lecture Notes in Computer Science, pages 488–501. Springer, 2004.
Marco Pistore, Marco Roveri, and Paolo Busetta. Requirements-driven verification of web services. Electr. Notes Theor. Comput. Sci., 105:95–108, 2004.
Alin Deutsch, Monica Marcus, Liying Sui, Victor Vianu, and Dayou Zhou. A verifier for interactive, data-driven web applications. In Fatma Ozcan, editor, Proceedings of the ACM SIGMOD International Conference on Management of Data, Baltimore, Maryland, USA, June 14-16, 2005, pages 539–550. ACM, 2005.
A. William Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1998.
Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.
Robin Milner, Joachim Parrow, and David Walker. A Calculus of Mobile Processes, I and II. Information and Computation, 100(1):1–40,41–77, September 1992.
Edmund M. Clarke, Sagar Chaki, Natasha Sharygina, Joel Ouaknine, and Nishant Sinha. State/event-based software model checking. In Proceedings of the International Conf. on Integrated Formal Methods, volume 2999 of Lecture Notes in Computer Science. Springer, 2004.
Rocco De Nicola and Frits W. Vaandrager. Three logics for branching bisimulation. Journal of the ACM (JACM), 42(2):458–487, 1995.
Ekkart Kindler and Tobias Vesper. ESTL: A temporal logic for events and states. In Application and Theory of Petri Nets 1998, 19th International Conference (ICATPN’98), volume 1420 of Lecture Notes in Computer Science, pages 365–383. Springer, 1998.
Michael Huth, Radha Jagadeesan, and David A. Schmidt. Modal transition systems: A foundation for three-valued program analysis. In Lecture Notes in Computer Science, volume 2028, page 155. Springer, 2001.
Aysu Betin-Can, Tevfik Bultan, and Xiang Fu. Design for verification for asynchronously communicating web services. In WWW ’05: Proceedings of the 14 th international conference on World Wide Web, pages 750–759, New York, NY, USA, 2005. ACM Press.
Dirk Beyer, Arindam Chakrabarti, and Thomas A. Henzinger. Web service interfaces. In WWW ’05: Proceedings of the 14 th international conference on World Wide Web, pages 148–159, New York, NY, USA, 2005. ACM Press.
Xiang Fu, Tevfik Bultan, and Jianwen Su. Realizability of conversation protocols with message contents. In ICWS, pages 96–. IEEE Computer Society, 2004.
Howard Foster, Sebastián Uchitel, Jeff Magee, and Jeff Kramer. Compatibility verification for web service choreography. In ICWS, pages 738–741. IEEE Computer Society, 2004.
David Booth, Hugo Haas, Francis McCabe, Eric Newcomer, Mike Champion, Christopher Ferris, and David Orchard. Web services architecture. World-Wide-Web Consortium (W3C). Available from http://www.w3.org/TR/ws-arch/, 2003.
David Detlefs, Greg Nelson, and James B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs, January 2003.
Edmund M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 154–169. Springer, 2000.
Thomas S. Anantharaman, Edmund M. Clarke, Michael J. Foster, and Bud Mishra. Compiling path expressions into VLSI circuits. In Proceedings of POPL, pages 191–204, 1985.
Himanshu Jain, Edmund M. Clarke, and Daniel Kroening. Verification of SpecC and Verilog using predicate abstraction. In Proceedings of MEMOCODE 2004, pages 7–16. IEEE, 2004.
Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, and Karen Yorav. Predicate abstraction of ANSI–C programs using SAT. Formal Methods in System Design, 25:105–127, September–November 2004.
Himanshu Jain, Daniel Kroening, Natasha Sharygina, and Edmund Clarke. Word level predicate abstraction and refinement for verifying RTL Verilog. In Proceedings of DAC 2005, pages 445–450. ACM, 2005.
Edmund Clarke, Orna Grumberg, Muralidhar Talupur, and Dong Wang. High level verification of control intensive systems using predicate abstraction. In First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE’03), pages 55–64. IEEE, 2003.
A. William Roscoe. The Theory and Practice of Concurrency. Prentice-Hall International, London, 1997.
Edmund M. Clarke, Himanshu Jain, and Daniel Kroening. Predicate Abstraction and Refinement Techniques for Verifying Verilog. Technical Report CMU-CS-04-139, 2004.
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Yhu. Symbolic model checking without BDDs. In TACAS, volume 1579 of Lecture Notes in Computer Science, pages 193–207. Springer, 1999.
David W. Currie, Alan J. Hu, and Sreeranga Rajan. Automatic formal verification of DSP software. In Proceedings of DAC 2000, pages 130–135. ACM Press, 2000.
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator: Beyond safety. In Computer Aided Verification, 18th International Conference, (CAV), volume 4144 of Lecture Notes in Computer Science, pages 415–418. Springer, 2006.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Sharygina, N., Kröning, D. (2007). Model Checking with Abstraction for Web Services. In: Baresi, L., Nitto, E.D. (eds) Test and Analysis of Web Services. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72912-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-72912-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72911-2
Online ISBN: 978-3-540-72912-9
eBook Packages: Computer ScienceComputer Science (R0)