A combined approach to checking web ontologies

ABSTRACT

The understanding of Semantic Web documents is built upon ontologies that define concepts and relationships of data. Hence, the correctness of ontologies is vital. Ontology reasoners such as RACER and FaCT have been developed to reason ontologies with a high degree of automation. However, complex ontology-related properties may not be expressible within the current web ontology languages, consequently they may not be checkable by RACER and FaCT. We propose to use the software engineering techniques and tools, i.e., Z/EVES and Alloy Analyzer, to complement the ontology tools for checking Semantic Web documents.In this approach, Z/EVES is first applied to remove trivial syntax and type errors of the ontologies. Next, RACER is used to identify any ontological inconsistencies, whose origins can be traced by Alloy Analyzer. Finally Z/EVES is used again to express complex ontology-related properties and reveal errors beyond the modeling capabilities of the current web ontology languages. We have successfully applied this approach to checking a set of military plan ontologies.

REFERENCES

• 1: Sean Bechhofer , Ian Horrocks , Carole A. Goble , Robert Stevens, OilEd: A Reason-able Ontology Editor for the Semantic Web, Proceedings of the Joint German/Austrian Conference on AI: Advances in Artificial Intelligence, p.396-408, September 19-21, 2001
• 2: T. Berners-Lee, J. Hendler, and O. Lassila. The Semantic Web. Scientific American, May 2001.
• 3: D. Brickley and R. Guha (editors). Resource description framework (rdf) schema specification 1.0. http://www.w3.org/TR/2000/CR-rdf-schema-20000327/, March, 2000.
• 4: J. Broekstra, M. Klein, S. Decker, D. Fensel, and I. Horrocks. Adding formal semantics to the web: building on top of rdf schema. In ECDL Workshop on the Semantic Web: Models, Architectures and Management, 2000.
• 5: M. Burstein, J. Hobbs, O. Lassila, D. Martin, S. McIlraith, S. Narayanan, M. Paolucci, T. Payne, K. Sycara, and H. Zeng. Daml service. http://www.daml.org/services/daml-s/2001/05/.
• 6: M. Dean, D. Connolly, F. van Harmelen, J. Hendler, I. Horrocks, D. L. McGuinness, P. F. Patel-Schneider, and L. A. Stein (editors). OWL Web Ontology Language 1.0 Reference. http://www.w3.org/TR/owl-ref/, 2002.
• 7: Jin Song Dong , Chew Hung Lee , Yuan Fang Li , Hai Wang, Verifying DAML+OIL and Beyond in Z/EVES, Proceedings of the 26th International Conference on Software Engineering, p.201-210, May 23-28, 2004
• 8: J. S. Dong, J. Sun, and H. Wang. Checking and Reasoning about Semantic Web through Alloy. In Proceedings of Formal Methods Europe: FME'03, volume 2805 of Lect. Notes in Comput. Sci., pages 796--814, Pisa, Italy, Sept. 2003. LNCS, Springer-Verlag.
• 9: Joseph A. Goguen , Rod M. Burstall, Institutions: abstract model theory for specification and programming, Journal of the ACM (JACM), v.39 n.1, p.95-146, Jan. 1992 [doi>10.1145/147508.147524]
• 10: V. Haarslev and R. Moller. Practical Reasoning in Racer with a Concrete Domain for Linear Inequations. In I. Horrocks and S. Tessaris, editors, Proceedings of the International Workshop on Description Logics (DL-2002), Toulouse, France, Apr. 2002. CEUR-WS.
• 11: V. Haarslev and R. Moller. RACER User's Guide and Reference Manual: Version 1.7.6, Dec. 2002.
• 12: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 13: Ian Horrocks, The FaCT System, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, p.307-312, May 05-08, 1998
• 14: D. Jackson. Micromodels of software: Lightweight modelling and analysis with Alloy. Available: http://sdg.lcs.mit.edu/alloy/book.pdf (an early version has been published in TOSEM Vol-11), 2002.
• 15: Daniel Jackson , Ian Schechter , Hya Shlyahter, Alcoa: the alloy constraint analyzer, Proceedings of the 22nd international conference on Software engineering, p.730-733, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337616]
• 16: P. Lambrix. Description Logics home page. http://www.ida.liu.se/labs/iislab/people/patla/DL/index.html.
• 17: C. H. Lee. Phase I Report for Plan Ontology. DSO National Labs, Singapore, 2002.
• 18: O. Lassila and R. R. Swick (editors). Resource Description Framework (RDF) Model and Syntax Specification. http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/, Feb, 1999.
• 19: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 20: Mark Saaltink, The Z/EVES System, Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation, p.72-85, April 03-04, 1997
• 21: Michael Sintek , Stefan Decker, TRIPLE - A Query, Inference, and Transformation Language for the Semantic Web, Proceedings of the First International Semantic Web Conference on The Semantic Web, p.364-378, June 09-12, 2002
• 22: Tim Berners-Lee. cwm - a general purpose data processor for the semantic web. http://www.w3.org/2000/10/swap/doc/cwm, 2004.
• 23: F. van Harmelen, P. F. Patel-Schneider, and I. Horrocks (editors). Reference description of the DAML+OIL ontology markup language. Contributors: T. Berners-Lee, D. Brickley, D. Connolly, M. Dean, S. Decker, P. Hayes, J. Heflin, J. Hendler, O. Lassila, D. McGuinness, L. A. Stein, ..., March, 2001.
• 24: Jim Woodcock , Jim Davies, Using Z: specification, refinement, and proof, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 25: World Wide Web Consortium (W3C). XSL Transformations (XSLT) Version 1.0. http://www.w3.org/TR/xslt, 1999.
• 26: World Wide Web Consortium (W3C). OWL Web Ontology Language Overview. http://www.w3.org/TR/owl-features/, Mar. 2003.
• 27: World Wide Web Consortium (W3C). Web Ontology Language (OWL) Use Cases and Requirements. http://www.w3.org/TR/webont-req/, Mar. 2003.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.4 Knowledge Representation Formalisms and Methods
          Subjects: Representation languages

General Terms:
Languages, Verification

Keywords:
alloy, daml+oil, ontologies, racer, semantic web, z