Derivation of ontological relations using formal methods in a situation awareness scenario

摘要

This paper describes a case study of relation derivation within the context of situation awareness. First we present a scenario in which inputs are supplied by a simulated Level 1 system. The inputs are events annotated with terms from an ontology for situation awareness. This ontology contains concepts used to represent and reason about situations. The ontology and the annotations of events are represented in DAML and Rule-ML and then systematically translated to a formal method language called MetaSlang. Having all information expressed in a formal method language allows us to use a theorem prover, SNARK, to prove that a given relationship among the Level 1 objects holds (or that it does not hold). The paper shows a proof of concept that relation derivation in situation awareness can be done within a formal framework. It also identifies bottlenecks associated with this approach, such as the issue of the large number of potential relations that may have to be considered by the theorem prover. The paper discusses ways of resolving this as well as other problems identified in this study.