Checking and Reasoning about Semantic Web through Alloy

v     Technical report ( TRB9/02, Sep 2002) on the topic is also available on-line: (postscript, pdf)

   Main approaches

   DAML+OIL semantic encoding

   DAML to Alloy Transformation

   Analyze DAML+OIL ontology

   Conclusions

   Acknowledgements

In recent years, researchers have begun to explore the potential of associating web content with explicit meaning so that the web content becomes more machine-readable and intelligent agents can retrieve and manipulate pertinent information readily. The Semantic Web (SW) proposed by W3C is one of the most promising and accepted approaches. It has been regarded as the next generation of the Web. SW not only emerges from the Knowledge Representation and the Web Communities, but also brings the two communities closer together. We believe there is a role for software engineering  techniques and tools to play and make important contributions to the SW development.

In the development of Semantic Web there is a pivotal role for ontology, since it provides a representation of a shared conceptualization of a particular domain that can be communicated between people and applications. Reasoning can be useful at many stages during the design, maintenance and deployment of ontology. Because autonomous software agents may perform their reasoning and come to conclusions without human supervision, it is essential that the shared ontology is consistent. However, since the Semantic Web technology is still in the early stage, the reasoning and consistency checking tools are very primitive.

The software modeling language Alloy is suitable for specifying structural properties of software. Alloy is a first order declarative language based on relations. We believe SW is a new novel application domain for Alloy because relationships between web resources are the focus points in SW. Furthermore, Alloy specifications can be analyzed automatically using the Alloy Analyzer (AA). Given a finite scope for a specification, AA translates it into a propositional formula and uses SAT solving technology to generate instances that satisfy the properties expressed in the specification. We believe that if the semantics of the SW languages can be encoded into Alloy, as a specification technique with fully automatic analysis supported then Alloy can be used to provide automatic reasoning and consistency checking services for SW. Various reasoning tasks can be supported effectively by AA. Some of those reasoning tasks are unique for AA, as currently no other SW reasoning tools can support those tasks.
 

In Our work we defined semantic model for the core DAML+OIL elements, so that analyzing DAML+OIL ontology in Alloy can be easily and effectively achieved. We also constructed a XSLT stylesheet for the automatic transformation from DAML+OIL file to into Alloy program. The main architecture of the system is are depictured by following Figure 1.

Figure 1: overall diagram

Supervisor :  Dr. DONG, Jin Song

Students :       SUN, Jing

                        WANG, Hai

Back to top

The DAML+OIL has a well-defined semantics which was described in a more expressive language. A set of axioms was added to this theory that constrains the models of the theory to all and only the intended interpretations. In this section based on the semantics of DAML+OIL, we define the semantic functions for the core DAML+OIL primitives in Alloy.

The whole semantic models for DAML+OIL are encoded in the module. Later users only need to import this module.

module DAMLOIL

All the things described in Semantic web context are called
resources. A basic type  Resource is defined as:
 

sig Resource {}
 

All other concepts defined later are extended from the  Recourse. Property, which is a kind of Resource itself, relates  Resource to  Resource.
 

disj sig Property extends Resource
{sub_val: Resource -> Resource}
 

Each  Property has a relation  sub_val of type  <Property, Resource, Resource>. This relation can be regarded as a statement, i.e., a triple of the form < property(or predicate), subject, value(or object)>, in the Semantic web. The class is corresponds to the generic concept of type or category of resource. Each  Class} maps a set of resources via the relation  instances}, which contains all the instance resources. The keyword  disj is used to indicate the Class and  Property are disjoined.

disj sig Class extends Resource
{instances: set Resource}
 

The DAML+OIL also allows the use of XML Schema datatypes to describe (or define) part of the datatype domain. However there are not any predefined types in Alloy, so we treat Datatype as a special Class, which contains all the possible datatype value in the instances relation.
 

disj sig Datatype extends Class {}

The  subClassOf is a relation between the classes. The instances in a subclass are also in the superclasses. A parameterized formula (a function in Alloy) is used to represent this concept.
 

fun subClassOf(csup, csub: Class)
{csub.instances in csup.instances}
 

The  disjointWith is a relation between the classes. It asserts that there is no instances common with each other.
fun disjoinWith( c1, c2: Class)
{ no c1.instances & c2.instances}

For the complete model please refer to the Technical report.

Back to top

In the previous section we defined semantic library for the core DAML+OIL elements, so that analyzing DAML+OIL ontology in Alloy can be easily and effectively achieved. We also constructed a XSLT stylesheet for the automatic transformation from DAML+OIL file to into Alloy program.
 

Back to top

Reasoning is one of the key tasks for semantic web. It can be useful at many stages during the design, maintenance and deployment of ontology.
There are two different level checking and reasoning, namely conceptual level and instance level. At conception level, we can reason about class properties and subclass relationships. At the instance level, we can do the membership checking (instantiation) and instance property reasoning. DAML reasoning tool, i.e. FaCT, can only provide conceptual level reasoning, while AA can perform both.
 

Back to top

The main contribution of this work is that it develops the semantic models for DAML+OIL language constructs in Alloy and the systematic transformation rules and (XSLT) program which can translate DAML ontology to Alloy automatically. With the assistance of Alloy Analyzer (AA), we also demonstrated that
the consistency of the SW ontology can be checked automatically and different kinds of
reasoning tasks can be supported. Alloy is chosen over other modeling techniques is mainly because

From a complete different direction, i.e., applying SW to build software modeling environment, we recently investigated how RDF and DAML can be used to construct a Semantic Web environment for supporting, extending and integrating various specification languages. We believe SW can contribute to the new developments for the software modeling environment.

In summary, there is a clear synergy between SW languages and software modeling techniques. The investigation between those two paradigms will lead great benefits for both areas.

Back to top

   Formal Design Methods and DAML from
      Defence Science & Technology Agency (DSTA) Singapore.
 

Back to top

Last revised: Friday, Sep 5, 2002.