Using KIV to specify and verify architectures of knowledge-based systems
Using KIV to specify and verify architectures of knowledge-based systems
复制标题
使用 KIV 指定和验证基于知识的系统的架构
DOI：
10.1109/ase.1997.632826
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
A. Schönegge
中科院分区：
文献类型：
--
作者：
D. Fensel;A. Schönegge
从可重用元素构建基于知识的系统是经济地开发它们的关键因素。但是，必须确保重用的构建块的假设和功能相互配合，并与实际问题和知识的具体情况相匹配。为此，我们使用卡尔斯鲁厄交互式验证器（KIV）。我们展示了如何用它来验证基于知识的系统的概念性和形式化规范。KIV最初是为程序程序的验证而开发的，但它也适用于验证基于知识的系统。其规范语言基于组件功能规范的抽象数据类型和算法规范的动态逻辑。它提供了一个集成到复杂工具环境中的交互式定理证明器，支持自动生成证明义务、生成反例、证明管理、证明重用等方面。这样的支持对于使复杂规范的验证变得可行是必不可少的。我们提供了一些关于如何指定和验证任务、解决问题的方法及其关系的示例。
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.