Semantic Web, the next generation of Web, gives data well-defined and machine-understandable meaning so that they can be processed by remote intelligent agents cooperatively. Ontology languages are the building blocks of Semantic Web as they prescribe how data are defined and related. The existing reasoning and verification tools for Semantic Web are improving however still elementary. We believe that Semantic Web can be a novel application domain for software modeling languages and tools. Z is a formal modeling language for specifying software systems and Z/EVES is a proof tool for Z. In this paper, we firstly present Z semantics for ontology language DAML+OIL. This semantic model is embedded as a Z section daml2zin Z/EVES, which serves as an environment for checking and verifying Web ontologies. Then we present a tool for automatically transforming ontology documents into the specialized Z codes understood by Z/EVES. Finally, we use a recent real application, the military plan ontologies, to demonstrate the different reasoning tasks that Z/EVES can perform. Furthermore, undiscovered errors in the original ontologies were found by Z/EVES and some of these errors are even beyond Semantic Web modeling and reasoning capabilities.

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.