The Community for Technology Leaders
RSS Icon
Issue No.03 - May-June (2012 vol.38)
pp: 592-608
Ivan Di Pietro , Università Politecnica delle Marche, Ancona
Francesco Pagliarecci , Università Politecnica delle Marche, Ancona
Luca Spalazzi , Università Politecnica delle Marche, Ancona
Model checking is a formal verification method widely accepted in the web service world because of its capability to reason about service behavior at process level. It has been used as a basic tool in several scenarios such as service selection, service validation, and service composition. The importance of semantics is also widely recognized. Indeed, there are several solutions to the problem of providing semantics to web services, most of them relying on some form of Description Logic. This paper presents an integration of model checking and semantic reasoning technologies in an efficient way. This can be considered the first step toward the use of semantic model checking in problems of selection, validation, and composition. The approach relies on a representation of services at process level that is based on semantically annotated state transition systems (asts) and a representation of specifications based on a semantically annotated version of computation tree logic (anctl). This paper proves that the semantic model checking algorithm is sound and complete and can be accomplished in polynomial time. This approach has been evaluated with several experiments.
Formal methods, model checking, temporal logic, description logic, intelligent web services, semantic web, web services.
Ivan Di Pietro, Francesco Pagliarecci, Luca Spalazzi, "Model Checking Semantically Annotated Services", IEEE Transactions on Software Engineering, vol.38, no. 3, pp. 592-608, May-June 2012, doi:10.1109/TSE.2011.10
[1] G. Alonso , F. Casati , H. Kuno , and V. Machiraju , Web Services - Concepts, Architectures and Applications. Springer, 2004.
[2] S. Hallé , R. Villemaire , and O. Cherkaoui , "Specifying and Validating Data-Aware Temporal Web Service Properties," IEEE Trans. Software Eng., vol. 35, no. 5, pp. 669-683, Sept./Oct. 2009.
[3] A. Barker , C.D. Walton , and D. Robertson , "Choreographing Web Services," IEEE Trans. Services Computing, vol. 2, no. 2, pp. 152-166, Apr.-June 2009.
[4] I. Di Pietro , F. Pagliarecci , L. Spalazzi , A. Marconi , and M. Pistore , "Semantic Web Service Selection at the Process-Level: The eBay/Amazon/PayPal Case Study," Proc. IEEE/WIC/ACM Int'l Conf. Web Intelligence and Intelligent Agent Technology, pp. 605-611, 2008.
[5] N. Milanovic and M. Malek , "Current Solutions for Web Service Composition," IEEE Internet Computing, vol. 8, no. 6, pp. 51-59, Nov./Dec. 2004.
[6] P. Traverso and M. Pistore , "Automated Composition of Semantic Web Services into Executable Processes," Proc. Int'l Semantic Web Conf., 2004.
[7] T. Sollazzo , S. Handschuh , S. Staab , M. Frank , and N. Stojanovic , "Semantic Web Service Architecture-Evolving Web Service Standards toward the Semantic Web," Proc. 15th Int'l Florida Artificial Intelligence Research Soc. Conf., S. Haller and G. Simmons, eds., pp. 425-429, 2002.
[8] K. Verma and A.P. Sheth , "Semantically Annotating a Web Service," IEEE Internet Computing, vol. 11, no. 2, pp. 83-85, Mar./Apr. 2007.
[9] S. McIlraith and S. Son , "Adapting Golog for Composition of Semantic Web Services," Proc. Int'l Conf. Knowledge Representation and Reasoning, 2002.
[10] D.L. McGuinness and E.F. van Harmelen , "OWL Web Ontology Language Overview," W3C, W3C Recommendation, /, 2004.
[11] Web Service Modeling Ontology (WSMO), H. Lausen, A. Polleres, and D. Roman, eds., W3C Member Submission,, June 2005.
[12] OpenTravel Implementation Guide—Version 1.1, OpenTravel Alliance, Boxborough, MA, USA, http:/, June 2009.
[13] Int'l Organization for Standardization "Information Technology —Business Operational View—Part 4: Business Transaction Scenarios—Accounting and Economic Ontology," ISO/IEC 15944-4:2000(E), Nov. 2007.
[14] Int'l Organization for Standardization "Information and Documentation—A Reference Ontology for the Interchange of Cultural Heritage Information," ISO 21127:2006, Sept. 2006.
[15] J. Euzenat and P. Shvaiko , Ontology Matching. Springer-Verlag, 2007.
[16] The Description Logic Handbook: Theory, Implementation, and Applications, F. Baader, D. Calvanese, D.L. McGuinness, D. Nardi, and P.F. Patel-Schneider, eds. Cambridge Univ. Press, 2003.
[17] E.A. Emerson , "Temporal and Modal Logic," Handbook of Theoretical Computer Science, J. van Leeuwen, ed., ch. 14, pp. 996-1072, Elsevier Science Publishers, 1990.
[18] A. Artale and E. Franconi , "A Survey of Temporal Extensions of Description Logics," Annals of Math. and Artificial Intelligence, vol. 30, nos. 1-4, pp. 171-210, 2000.
[19] C. Lutz , F. Wolter , and M. Zakharyaschev , "Temporal Description Logics: A Survey," Proc. 15th Int'l Symp. Temporal Representation and Reasoning, S. Demri and C. Jensen, eds., pp. 3-14, 2008.
[20] A. Cimatti , E.M. Clarke , F. Giunchiglia , and M. Roveri , "NuSMV: A New Symbolic Model Checker," Int'l J. Software Tools for Technology Transfer, vol. 2, no. 4, pp. 410-425, 2000.
[21] M. Pistore , L. Spalazzi , and P. Traverso , "A Minimalist Approach to Semantic Annotations for Web Processes Compositions," Proc. Third European Semantic Web Conf., 2006.
[22] P. Bertoli , A. Cimatti , M. Pistore , M. Roveri , and P. Traverso , "MBP: A Model Based Planner," Proc. IJCAI '01 Workshop Planning under Uncertainty and Incomplete Information, 2001.
[23] F. Giunchiglia and I. Zaihrayeu , "Lightweight Ontologies," Technical Report DIT-07-071, DIT, Univ. of Trento, Oct. 2007.
[24] D. Calvanese , G. De Giacomo , D. Lembo , M. Lenzerini , and R. Rosati , "Data Complexity of Query Answering in Description Logics," Proc. 10th Int'l Conf. Principles of Knowledge Representation and Reasoning, 2006.
[25] S.S. Lam and A.U. Shankar , "A Relational Notation for State Transition Systems," IEEE Trans. Software Eng., vol. 16, no. 7, p. 755, July 1990.
[26] E.M. Clarke and J.M. Wing , "Formal Methods: State of the Art and Future Directions," ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, Dec. 1996.
[27] M. Ortiz , D. Calvanese , and T. Eiter , "Characterizing Data Complexity for Conjunctive Query Answering in Expressive Description Logics," Proc. 21st Nat'l Conf. Artificial Intelligence, pp. 275-280, 2006.
[28] E.A. Emerson , "Model Checking and the Mu-Calculus," Proc. Descriptive Complexity and Finite Models DIMACS Workshop, N. Immerman and P.G. Kolaitis, eds., vol. 31, pp. 185-214, 1996.
[29] A. Artale , R. Kontchakov , C. Lutz , F. Wolter , and M. Zakharyaschev , "Temporalising Tractable Description Logics," Proc. 14th Int'l Symp. Temporal Representation and Reasoning, pp. 11-22, 2007.
[30] J.R. Burch , E.M. Clarke , K.L. McMillan , D.L. Dill , and L.J. Hwang , "Symbolic Model Checking: $10^{20}$ States and Beyond," Information and Computation, vol. 98, no. 2, pp. 142-170, June 1992.
[31] S. Agarwal , "Formal Description of Web Services for Expressive Matchmaking," PhD dissertation, Fakultät für Wirtschaftswissenschaften, Universität Karlsruhe (TH), 2007.
[32] F. Weitl , M. Jakšić , and B. Freitag , "Towards the Automated Verification of Semi-Structured Documents," J. Data and Knowledge Eng., vol. 68, pp. 292-317, 2009.
[33] G. Holzmann , The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004.
[34] P. Schnoebelen , "The Complexity of Temporal Logic Model Checking," Proc. Int'l Workshop Advances in Modal Logic, P. Balbiani, N.-Y. Suzuki, F. Wolter, and M. Zakharyaschev, eds., pp. 393-436, 2002.
[35] X. Zhang and Z. Lin , "An Argumentation-Based Approach to Handling Inconsistencies in DL-Lite," Proc. Ann. German Conf. Advances in Artificial Intelligence, B. Mertsching, M. Hund, and M.Z. Aziz, eds., pp. 615-622, 2009.
[36] M. Fischer and R. Ladner , "Propositional Modal Logic of Programs," J. Computer and Systems Sciences, vol. 18, pp. 194-211, 1979.
[37] M.Y. Vardi , "Automata-Theoretic Techniques for Temporal Reasoning," Handbook of Modal Logic, P. Blackburn, J. van Benthem, and F. Wolter, eds., pp. 971-989, Elsevier, 2006.
[38] E.M. Clarke , E.A. Emerson , and A.P. Sistla , "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, Apr. 1986.
[39] A. Rabinovich , "Symbolic Model Checking for $\mu$ -Calculus Requires Exponential Time," Theoretical Computer Science, vol. 243, pp. 467-475, 2000.
[40] R.E. Bryant , "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, vol. 35, no. 8, pp. 677-691, Aug. 1986.
[41] E. Sirin , B. Parsia , B. Cuenca Grau , A. Kalyanpur , and Y. Katz , "Pellet: A Practical OWL-DL Reasoner," Web Semantics: Science, Services and Agents on the World Wide Web, vol. 5, no. 2, pp. 51-53, 2007.
[42] F. Baader , A. Bauer , and M. Lippmann , "Runtime Verification Using a Temporal Description Logic," Proc. Seventh Int'l Symp. Frontiers of Combining Systems, pp. 149-164, 2009.
[43] S. Agarwal , "A Goal Specification Language for Automated Discovery and Composition of Web Services," Proc. Int'l Conf. Web Intelligence, 2007.
[44] A. Deutsch , L. Sui , V. Vianu , and D. Zhou , "Verification of Communicating Data-Driven Web Services," Proc. 25th ACM SIGMOD-SIGACT-SIGART Symp. Principles of Database Systems, pp. 90-99, 2006.
[45] T. Andrews , F. Curbera , H. Dolakia , J. Goland , J. Klein , F. Leymann , K. Liu , D. Roller , D. Smith , S. Thatte , I. Trickovic , and S. Weeravarana , "Business Process Execution Language for Web Services (version 1.1)," 2003.
[46] T.O.S. Coalition , "OWL-S: Semantic Markup for Web Services," 2003.
[47] S. Narayanan and S. McIlraith , "Simulation, Verification and Automated Composition of Web Services," Proc. Int'l Conf. World Wide Web, 2002.
[48] R. Hull , M. Benedikt , V. Christophides , and J. Su , "E-Services: A Look behind the Curtain," Proc. ACM SIGMOD-SIGACT-SIGART Symp. Principles of Database Systems, 2003.
[49] D. Berardi , D. Calvanese , G.D. Giacomo , M. Lenzerini , and M. Mecella , "Automatic Composition of E-Services that Export Their Behaviour," Proc. Int'l Joint Conf. Service Oriented Computing, 2003.
[50] M. Pistore , A. Marconi , P. Bertoli , and P. Traverso , "Automated Composition of Web Services by Planning at the Knowledge Level," Proc. Int'l Joint Conf. Artificial Intelligence, 2005.
[51] D. Mandell and S. McIlraith , "Adapting BPEL4WS for the Semantic Web: The Bottom-Up Approach to Web Service Interoperation," Proc. Second Int'l Semantic Web Conf., 2003.
[52] D. Wu , B. Parsia , E. Sirin , J. Hendler , and D. Nau , "Automating DAML-S Web Services Composition Using SHOP2," Proc. Int'l Semantic Web Conf., 2003.
[53] M. Sheshagiri , M. desJardins , and T. Finin , "A Planner for Composing Services Described in DAML-S," Proc. Workshop Web Services and Agent-Based Eng., 2003.
[54] M.H. Burstein , J.R. Hobbs , O. Lassila , D.L. Martin , D.V. McDermott , S.A. McIlraith , S. Narayanan , M. Paolucci , T.R. Payne , and K.P. Sycara , "DAML-S: Web Service Description for the Semantic Web," Proc. Int'l Semantic Web Conf., I. Horrocks and J.A. Hendler, eds., pp. 348-363, 2002.
[55] Web Service Modeling Language (WSML), J. de Bruijn and H. Lausen, eds., W3C Member Submission, http://www., June 2005.
[56] S. Tobies , "Complexity Results and Practical Algorithms for Logics in Knowledge Representation," PhD dissertation, RWTH Aachen, 2001.
[57] A. Patil , S. Oundhakar , A. Sheth , and K. Verma , "METEOR-S Web Service Annotation Framework," Proc. Int'l Conf. World Wide Web, 2004.
[58] K. Verma , A. Mocan , M. Zarembra , A. Sheth , and J.A. Miller , "Linking Semantic Web Service Efforts: Integrating WSMX and METEOR-S," Proc. Int'l Workshop Semantic and Dynamic Web Processes, 2005.
[59] A. Sheth , K. Verna , J. Miller , and P. Rajasekaran , "Enhacing Web Service Descriptions Using WSDL-S," Proc. EclipseCon, 2005.
[60] W3C Semantic Annotations for Web Service Description Language Working Group "Semantic Annotations for WSDL and XML Schema," 2007.
[61] I. Di Pietro , F. Pagliarecci , and L. Spalazzi , "Semantic Annotation for Web Service Processes in a Pervasive Computing," Pervasive Computing: Innovations in Intelligent Multimedia and Applications, A. Hassanien, A. Abraham, H. Hagras, and J.H. Abawajy, eds., Springer-Verlag, 2009.
[62] L. Boaro , E. Glorio , F. Pagliarecci , and L. Spalazzi , "Model Checking Security Requirements for Web Services," Proc. Int'l Conf. High Performance Computing Simulation, June 2010.
[63] T. Leo , F. Pagliarecci , and L. Spalazzi , "eLearning for Complex System Professionals: Material Knowledge Representation, Retrieval, and Building," Proc. Fourth Int'l Forum on Knowledge Asset Dynamics, Feb. 2009.
26 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool