In order to automatically find and conveniently rectify the structural conflicts appearing in a new ontology model version after a series of ontology evolution,we propose an ontology model verification approach,in whi...In order to automatically find and conveniently rectify the structural conflicts appearing in a new ontology model version after a series of ontology evolution,we propose an ontology model verification approach,in which the object constraint language (OCL) and an ontology definition meta-model (ODM) are used to complete the ontology verification.The ODM is composed of the ontology related elements and the definition rule related elements.The OCL is employed to describe the elements in the ontology definition meta-model:OCL extension for the ontology related elements,and OCL extension for the ontological design patterns.All of the above OCL rules will describe the constraint relationships between ontology elements.Associated with an example,the application of the ontology model verification approach based on OCL and ODM is introduced.Consequently,the conflicts happened in the ontology changing and evolution can be easily verified and rectified through this approach.展开更多
Checking whether a given formula is an invariant at a given program location(especially,inside a loop) can be quite nontrivial even for simple loop programs,given that it is in general an undecidable property.This is ...Checking whether a given formula is an invariant at a given program location(especially,inside a loop) can be quite nontrivial even for simple loop programs,given that it is in general an undecidable property.This is especially the case if the given formula is not an inductive loop invariant,as most automated techniques can only check or generate inductive loop invariants.In this paper,conditions are identified on simple loops and formulas when this check can be performed automatically.A general theorem is proved which gives a necessary and sufficient condition for a formula to be an invariant under certain restrictions on a loop.As a byproduct of this analysis,a new kind of loop invariant inside the loop body,called inside-loop invariant,is proposed.Such an invariant is more general than an inductive loop invariant typically used in the Floyd-Hoare axiomatic approach to program verification.The use of such invariants for program debugging is explored;it is shown that such invariants can be more useful than traditional inductive loop invariants especially when one is interested in checking extreme/side conditions such as underflow,accessing array/collection data structures outside the range,divide by zero,etc.展开更多
基金Sponsored by the National Basic Research Program of China (the Natural Key Basis Research and Development Plan (Grant No.973:2003CB316905))the National Natural Science Foundation of China(Grant No.60374071)
文摘In order to automatically find and conveniently rectify the structural conflicts appearing in a new ontology model version after a series of ontology evolution,we propose an ontology model verification approach,in which the object constraint language (OCL) and an ontology definition meta-model (ODM) are used to complete the ontology verification.The ODM is composed of the ontology related elements and the definition rule related elements.The OCL is employed to describe the elements in the ontology definition meta-model:OCL extension for the ontology related elements,and OCL extension for the ontological design patterns.All of the above OCL rules will describe the constraint relationships between ontology elements.Associated with an example,the application of the ontology model verification approach based on OCL and ODM is introduced.Consequently,the conflicts happened in the ontology changing and evolution can be easily verified and rectified through this approach.
基金supported by NSFC-90718041NKBRPC-2005C B321902+1 种基金China Scholarship Council in Chinasupported by the National Science Foundation award CCF-0729097
文摘Checking whether a given formula is an invariant at a given program location(especially,inside a loop) can be quite nontrivial even for simple loop programs,given that it is in general an undecidable property.This is especially the case if the given formula is not an inductive loop invariant,as most automated techniques can only check or generate inductive loop invariants.In this paper,conditions are identified on simple loops and formulas when this check can be performed automatically.A general theorem is proved which gives a necessary and sufficient condition for a formula to be an invariant under certain restrictions on a loop.As a byproduct of this analysis,a new kind of loop invariant inside the loop body,called inside-loop invariant,is proposed.Such an invariant is more general than an inductive loop invariant typically used in the Floyd-Hoare axiomatic approach to program verification.The use of such invariants for program debugging is explored;it is shown that such invariants can be more useful than traditional inductive loop invariants especially when one is interested in checking extreme/side conditions such as underflow,accessing array/collection data structures outside the range,divide by zero,etc.
