Modular verification of web services using efficient symbolic encoding and summarization

ABSTRACT

We propose a novel method for modular verification of web service compositions. We first use symbolic fixpoint computations to derive conditions on the incoming messages and relations among the incoming and outgoing messages of individual BPEL web services. These pre- and post-conditions are accumulated and serve as a repository of summarizations of individual web services. We then compose the summaries of the invoked BPEL services to model external invocations, resulting in a scalable verification approach for web service compositions. Our technical contributions include (1) an efficient symbolic encoding for modeling the concurrency semantics of systems having both multi-threading and message passing, and (2) a scalable method for summarizing concurrent processes that interact with each other using synchronous message passing, along with a modular framework that utilizes these summaries for scalable verification.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger , Freddy Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, MOCHA: Modularity in Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.521-525, June 28-July 02, 1998
• 2: Dirk Beyer , Arindam Chakrabarti , Thomas A. Henzinger, Web service interfaces, Proceedings of the 14th international conference on World Wide Web, May 10-14, 2005, Chiba, Japan [doi>10.1145/1060745.1060770]
• 3: Tevfik Bultan , Richard Gerber , Christopher League, Composite model-checking: verification with type-specific symbolic representations, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.3-50, Jan. 2000 [doi>10.1145/332740.332746]
• 4: S. Chaki , E. Clarke , A. Groce , J. Ouaknine , O. Strichman , K. Yorav, Efficient Verification of Sequential and Concurrent C Programs, Formal Methods in System Design, v.25 n.2-3, p.129-166, September-November 2004 [doi>10.1023/B:FORM.0000040026.56959.91]
• 5: Rance Cleaveland , Steve Sims, The NCSU Concurrency Workbench, Proceedings of the 8th International Conference on Computer Aided Verification, p.394-397, August 03, 1996
• 6: J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. Learning assumptions for compositional verification. In Tools and Algorithms for the Construction and Analysis of Systems, pages 331--346. Springer, 2003. LNCS 2619.
• 7: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 8: Ziyang Duan , Arthur Bernstein , Philip Lewis , Shiyong Lu, A model for abstract process specification, verification and composition, Proceedings of the 2nd international conference on Service oriented computing, November 15-19, 2004, New York, NY, USA [doi>10.1145/1035167.1035201]
• 9: Ziyang Duan , Arthur Bernstein , Philip Lewis , Shiyong Lu, Semantics Based Verification and Synthesis of BPEL4WS Abstract Processes, Proceedings of the IEEE International Conference on Web Services, p.734, June 06-09, 2004 [doi>10.1109/ICWS.2004.98]
• 10: Javier Esparza , Andreas Podelski, Efficient algorithms for pre* and post* on interprocedural parallel flow graphs, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325697]
• 11: J. Klein F. Leymann D. Roller F. Curbera, Y. Goland and S. Weerawarana. Business process execution language for web services, version 1.1. 2003.
• 12: R. Farahbod, U. Glässer, and M. Vajihollahi. An abstract machine architecture for web service based business process management. In Business Process Management, pages 144--157. Springer, 2005. LNCS 3812.
• 13: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338 n.1-3, p.153-183, 10 June 2005 [doi>10.1016/j.tcs.2004.12.006]
• 14: Howard Foster , Sebastian Uchitel , Jeff Magee , Jeff Kramer, Compatibility Verification for Web Service Choreography, Proceedings of the IEEE International Conference on Web Services, p.738, June 06-09, 2004 [doi>10.1109/ICWS.2004.36]
• 15: Xiang Fu , Tevfik Bultan , Jianwen Su, Analysis of interacting BPEL web services, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA [doi>10.1145/988672.988756]
• 16: Xiang Fu , Tevfik Bultan , Jianwen Su, Model checking XML manipulating software, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 17: S. Haddad, T. Melliti, P. Moreaux, and S. Rampacek. Modelling web services interoperability. In International Conference on Enterprise Information Systems, pages 287--295, 2004.
• 18: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 19: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 20: K. Huynh. Analysis through reflction: walking the EMF model of BPEL4WS. Master's thesis, York University, Toronto, Canada, 2005.
• 21: N. Lohmann, P. Massuthe, C. Stahl, and D. Weinberg. Analyzing interacting bpel processes. In Business Process Management, pages 17--32. Springer, 2006. LNCS 4102.
• 22: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 23: S. Nakajima. Model-checking behavioral specification of BPEL applications. Electr. Notes Theor. Comput. Sci., 151(2):89--105, 2006.
• 24: Shaz Qadeer , Sriram K. Rajamani , Jakob Rehof, Summarizing procedures in concurrent programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-255, January 14-16, 2004, Venice, Italy
• 25: Z. Qiu, S. Wang, G. Pu, and X. Zhao. Semantics of BPEL4WS-like fault and compensation handling. In International Symposium of Formal Methods, pages 350--365. Springer, 2005. LNCS 3582.
• 26: R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. May 1995.
• 27: N. Sharygina K. Wallnau S. Chaki, J. Ivers. The comfort reasoning framework. In Computer Aided Verification, pages 164--169, 2005.
• 28: N. Sharygina, S. Chaki, E. M. Clarke, and N. Sinha. Dynamic component substitutability analysis. In International Symposium of Formal Methods Europe, pages 512--528. Springer, 2005. LNCS 3582.
• 29: Z. Yang, C. Wang, F. Ivančić, and A. Gupta. Mixed symbolic representations for model checking software programs. In Formal Methods and Models for Codesign, pages 17--24, July 2006.
• 30: T. Yavuz-Kahveci and T. Bultan. A symbolic manipulator for automated verification of reactive systems with heterogeneous data types. STTT, 5(1):15--33, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
BPEL, modular verification, summarization