LINK [1] T. Ball and S.K. Rajamani, “The SLAM Project: Debugging System Software via Static Analysis,” In Proc. POPL 2002, pp.1-3, Jan. 2002.

LINK [2] M. A. Bishop, Computer Security: Art and Science, Addison-Wesley, 2003.

LINK [3] F. van Breugel and M. Koshkina, “Does Dead-Path-Elimination have Side Effects?,” Technical Report CS-2003-04, York Univ., Apr. 2003.

LINK [4] A. Brogi, C. Canal, E. Pimentel, and A. Vallecillo, “Formalizing Web Service Choreographies,” In Proc. WSFM 2004, pp.73-94, Feb. 2004.

LINK [5] E. Christensen, F. Curbera, G. Meredith, and S. Weerawarana, “Web Service Description Language(WSDL),” W3C Web Site, 2001.

LINK [6] E. Clarke, O. Grumberg, and D. Peled, Model Checking, The MIT Press, 1999.

LINK [7] F. Curbera, Y. Goland, J. Klein, F. Leymann, D. Roller, S. Thatte, and S. Weerawarana, Business Process Execution Language for Web Services, Version 1.1, May 2003.

LINK [8] F. Curbera, R. Khalaf, N. Mukhi, S. Tai, and S. Weerawarana, “The Next Step in Web Services,” Commun. ACM, vol. 46, no. 10, pp.29-34, Oct. 2003.

LINK [9] H. Foster, S. Uchitel, J. Magee, and J. Kramer, “Model-based Verification of Web Service Compositions,” Proc. ASE 2003, Sept. 2003.

LINK [10] H. Foster, S. Uchitel, J. Magee, and J. Kramer, “Compatibility Verification for Web Service Choreogrphy,” In Proc. ICWS’04, July 2004.

LINK [11] X. Fu, T. Bultan, and J. Su, “Analysis of Interacting BPEL Web Services,” In Proc. WWW 2004, pp.621-630, May 2004.

LINK [12] S. Graf and H. Saidi, “Construction of Abstract State Graphs with PVS,” In Proc. CAV’97, pp.72-83, 1997.

LINK [13] G. J. Holzmann, The SPIN Model Checker, Addison-Wesley, 2004.

LINK [14] D. Jackson and J. Wing, “Lightweight Formal Methods,” In An Invitation to Formal Methods (Ed. H. Saiedian), IEEE Computer, vol.29, no.4,pp.16-30, Apr. 1996.

LINK [15] K. Jensen, Coloured Petri Nets 1, Springer-Verlag, 1992.

LINK [16] M. Koshkina and F. van Breugel, “Verification of Business Processes forWeb Services,” Technical Report CS-2003-11, York Univ., Oct. 2003.

LINK [17] F. Leymann and W. Altenhuber, “Managing Business Processes as an Information Resource,” IBM System Journal, vol.33, no.2, pp.326-348, 1994.

LINK [18] F. Leymann and D. Roller, Production Workflow: concepts and techniques, Prentice Hall, 1999.

LINK [19] F. Leymann, Web Services Flow Language (WSFL 1.0), IBM Corporation, May, 2001.

LINK [20] J. Magee and J. Kramer, Concurrency-State Model & Java Programs, Wiley, 1999.

LINK [21] M. Mazzara and R. Lucchi, “A Framework for Generic Error Handling in Business Processes,” In Proc. WSFM 2004, pp.133-145, Feb. 2004.

LINK [22] L.G. Meredith and S. Bjorg, “Contracts and Types,”Commun. ACM, vol. 46, no. 10, pp.41-47, Oct. 2003.

LINK [23] S. Nakajima, “On Verifying Web Service Flows,” InProc. SAINT 2002 Workshop, pp.223-224, Jan. 2002.

LINK [24] S. Nakajima, “Verification of Web Service Flows with Model-Checking Techniques,” In Proc. Cyber World 2002, pp.378-385, IEEE, Nov. 2002.

LINK [25] S. Nakajima, “Model-Checking of Web Service Flow (in Japanese),” In Trans. IPS Japan, vol.44, no.3, pp.942-952, Mar. 2003. A concise version presented at OOPSLA 2002 Workshop on Object-Oriented Web Service, Nov. 2002.

LINK [26] S. Nakajima, “Model-Checking of Safety and Security Aspects in Web Service Flows,” In Proc. ICWE’04, July 2004.

LINK [27] S. Nakajima, “Model-Checking Behavioral Specification of BPEL Applications,” In Proc. WLFM’05, July 2005.

LINK [28] S. Narayanan and S. A. Mcllraith, “Simulation, Verification and Automated Composition of Web Services,” In Proc. WWW-11, 2002.

LINK [29] G. Salaun, L. Bordeaux, and M. Schaerf, “Describing and Reasoning on Web Services using Process Alge bra,” In Proc. ICWS’04, July 2004.

LINK [30] B. Sarna-Starosta and C. R. Ramakrishnan, “Constraint-Based Model Checking of Data-Independent System,” In ICFEM’03, 2003.

LINK [31] M.P.Singh and M.N.Huhns, Service-Oriented Computing, Wiley, 2005.

LINK [32] S. Thatte, XLANG-Web Services for Business Process Design, Microsoft Corporation, May, 2001.

LINK [33] UDDI Web Site, UDDI Technical White Paper.
http://www.uddi.org , Sept. 2000.

LINK [34] W. Visser, S. Park, and J. Penix, “Using Predicate Abstraction to Reduce Object-Oriented Programs for Model Checking,” In Proc. FMSP ’00, 2000.

LINK [35] G. Weikum and G. Vossen, Transactional Information Systems, Morgan Kaufmann, 2002.

LINK [36] Workflow Management Coalition, “Interface 1: Process Definition Language Process Model,” WfMC TC-1016-P (v1.1), Oct. 1999.

LINK [37] P. Wohed, W. van der Aalst, M.Dumas, and A. ter Hofstede, “Pattern Based Analysis of BPEL4WS”, Tech. Rep. FIT-TR-2002-04, EUT, 2002.

LINK [38] A. Wombacher, P. Frankhauser, and E. Neuhold, “Transforming BPEL into annotated Deterministic Finite State Automata for Service Discovery,” In Proc. ICWS’04, July, 2004.

LINK [39] P. Wolper, “Expressing Interesting Properties of Programs in Propositional Temporal Logic,” In Proc. POPL’86, Jan. 1986.