Published: 1997 Juni
Buchtitel: Proceedings of the 9th International Conference on Software Engineering & Knowledge Engineering (SEKE'97), Madrid, Spain, June 18-20, 1997
The paper introduces an approach for the specification and verification of knowledge-based systems that combines conceptual and formal techniques. We identify four elements of the specification of a knowledge-based system: a task definition, a problem-solving method, a domain model, and an adapter that relates the other elements. We present abstract data types and a variant of dynamic logic as formal means to specify and verify these different elements. As a consequence of our conceptual model we can decompose the overall verification task of the knowledge-based systems into different proof obligations. Each proof obligation deals with a different aspect of the entire system. The use of the conceptual model in specification and verification improves understandability and reduces the effort for both activities. The modularization enables reuse of specifications and proofs. A knowledge-based system can be build by combing and adapting different components.