The University of Queensland Homepage
UQ HomepageSearch UQFind all Contacts at UQStudy Options at UQEvents at UQUQ MapsUQ LibraryLink to my.UQ
School of ITEE ITEE Main Website
      





  LI, Yuan Fang's Thesis Page

Thesis information

Title: A Formal Modeling Approach to Ontology Engineering – Modeling, Transformation & Verification

Advisor: A/P DONG, Jin Song

Abstract: The Semantic Web has been regarded by many as the new generation of the World Wide Web. It enables software agents on the Web to autonomously and collaboratively understand, process and aggregate information by giving Web resources well-defined and machine-interpretable markups, in the form of ontologies. Ensuring the correctness of ontologies is very important as inconsistent ontologies may lead software agents to reason erroneously. Such tasks are non trivial as the more expressive ontology languages are, the less automated are the reasoners/provers and with the growth of the size of ontologies, locating inconsistencies is also more difficult. Further, as the expressivity of these languages is also limited in more than one way, certain desirable ontology-related properties cannot be expressed in these languages. The ability to express and check these properties will make ontologies more accurate and more robust. It is therefore highly desirable. Dynamic Web services help make the Web truly ubiquitous. In the Semantic Web, service ontologies describe the capabilities, requirements, control structures, etc., of Web services. Their consistency must also be guaranteed to ensure the correct functioning of software agents. Software engineering and in particular formal methods are an active and well-developed research area. We believe that mature formal methods and their tool support can contribute to the development of the Semantic Web. This thesis presents a formal modeling approach for verifying ontologies. By defining semantics of ontology languages in expressive formal languages, their proof tools can be used to ensure the correctness of ontology-related properties. The validity of the above approach entirely relies on the correctness of the semantics of ontology languages in formal methods. Hence, the other important topic in this thesis is the proof of such correctness. An abstract approach using institutions and institution morphisms is employed to represent and reason about ontology languages and formal languages. An integrated tools environment is also presented to facilitate the application of the verification approach.

Keywords: Semantic Web, DAML+OIL, institutions, ontology, OWL, verification, Z, LSC

Download

  • 1.5-spacing (200 pages): pdf, ps.gz.
  • Double-spacing (240 pages): pdf, ps.gz.
  • Individual chapters (1.5-spacing) can be downloaded below.

Table of contents

Thanks...

The thesis received the following funding and awards:

  • "Defense Innovative Research Project (DIRP) - Formal Methods and DAML" - Defense Science & Technology Agency (DSTA) Singapore.
  • Singapore Millennium Foundation (SMF) Ph.D. Scholarship
  • President's Graduate Fellowship, National University of Singapore
  • The Advanced Study Institute, NATO Science Committee
  • SIGSOFT Student Funding, ACM
  • Dean's award, School of Computing, National University of Singapore

Selected publications from the thesis

  • D. Lucanu, Y.-F. Li, J. S. Dong. Semantic Web Languages - Towards an Institutional Perspective. In Algebra, Meaning, and Computation: A Festschrift in Honor of Prof. Joseph Goguen, Eds. Futatsugi, Jouannaud, and Meseguer, pages 99-123, 2006. LNCS 4060, Springer-Verlag. [bib]

  • J. Sun, Y.-F. Li, H. Wang and J. Sun. Visualizing and Simulating Semantic Web Services Ontologies. In 7th International Conference on Formal Engineering Methods (ICFEM'05), pages 435-449, Manchester, United Kingdom , November 2005. LNCS, Springer-Verlag. [bib]

  • D. Lucanu, Y.-F. Li and J. S. Dong. Institution Morphisms for Relating OWL and Z. In 17th International Conference on Software Engineering and Knowledge Engineering (SEKE'05), Taipei, Taiwan, July 2005. [bib]

  • J. S. Dong, C. H. Lee, H. B. Lee, Y.-F. Li and H. Wang. A Combined Approach to Checking Web Ontologies. In 13th ACM International World Wide Web Conference (WWW'04), pages 714-722, ACM Press, New York, USA, May 2004. [bib]

  • J. S. Dong, C. H. Lee, Y.-F. Li and H. Wang. Verifying DAML+OIL and Beyond in Z/EVES. In 26th International Conference on Software Engineering (ICSE'04), pages 201-210, ACM/IEEE Press, Edinburgh, Scotland, UK, May 2004. [bib]

  • J. S. Dong, Y.-F. Li, J. Sun, J. Sun and H. Wang. XML-based static type checking and dynamic visualization for TCOZ. In 4th International Conference on Formal Engineering Methods (ICFEM'02), pages 311-322, Shanghai, China, Oct 2002. [bib]

Last updated: 8 September, 2008
© 2002-2009 The University of Queensland, Brisbane, Australia
ABN 63 942 912 684
CRICOS Provider No: 00025B

This is a personal web area hosted on a University of Queensland web server.
Please be advised that this web page is not officially endorsed by The University of Queensland.
The University accepts no responsibility or liability for the contents of this area.

Last Updated: 8 September, 2008, 1:23pm