Inproceedings599
Using KIV to Specify and Verify Architectures of Knowledge-Based Systems
Using KIV to Specify and Verify Architectures of Knowledge-Based Systems
Published: 1997
November
Buchtitel: Proceedings of the 12th IEEE International Conference on Automated Software Engineering (ASEC-97), Incline Village, Nevada, November 3-5, 1997
Referierte Veröffentlichung
BibTeX
Kurzfassung
Building knowledge-based systems from reusable elements is a key factor in their economic development. However, one has to ensure that the assumptions and functionality of the reused building block fit to 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 done with it. KIV was originally developed for the verification of procedural programs but it fits well for verifying knowledge-based systems. Its specification language is based on algebraic specification means 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 in making verification of complex specifications feasible. We provide some examples on how to specify and verify tasks, problem-solving methods, and their relationships.
An earlier version was appeared as: Specifying and Verifying Knowledge-Based Systems with KIV. In Proceedings of the European Symposium on the Validation and Verification of Knowledge Based Systems EUROVAV-97, Leuven Belgium, June 26-28, 1997.
Download: Media:1997_599_Fensel_Using_KIV_to_Sp_1.ps.gz