Title :
Using KIV to specify and verify architectures of knowledge-based systems
Author :
Fensel, Dieter ; Schnogge, A.
Author_Institution :
Inst. fur Angewandte Inf. und Formale Beschreibungsverfahren, Karlsruhe Univ., Germany
Abstract :
Building knowledge-based systems from reusable elements is a key factor in developing them economically. However, one has to ensure that the assumptions and functionality of the reused building block fit together with each other and the specific circumstances of the actual problem and knowledge. We use the Karlsruhe Interactive Verifier (KIV) for this purpose. We show how the verification of conceptual and formal specifications of knowledge-based systems can be performed with it. KIV was originally developed for the verification of procedural programs but it serves well for verifying knowledge-based systems. Its specification language is based on abstract data types for the functional specification of components and dynamic logic for the algorithmic specification. It provides an interactive theorem prover integrated into a sophisticated tool environment supporting aspects like the automatic generation of proof obligations, generation of counter examples, proof management, proof reuse etc. Such a support is essential for making the verification of complex specifications feasible. We provide some examples on how to specify and verify tasks, problem-solving methods, and their relationships
Keywords :
abstract data types; formal specification; formal verification; knowledge based systems; theorem proving; Karlsruhe interactive verifier; abstract data types; algorithmic specification; dynamic logic; formal specifications; functional specification; interactive theorem prover; knowledge-based systems; proof management; proof reuse; reusable elements; specification language; Buildings; Computer architecture; Counting circuits; Environmental management; Knowledge based systems; Knowledge engineering; Logic; Problem-solving; Software architecture; Terminology;
Conference_Titel :
Automated Software Engineering, 1997. Proceedings., 12th IEEE International Conference
Conference_Location :
Incline Village, NV
Print_ISBN :
0-8186-7961-1
DOI :
10.1109/ASE.1997.632826