TY - GEN
T1 - Compositional verification of knowledge-based systems: A case study for diagnostic reasoning
AU - Cornelissen, F.J.
AU - Jonker, C.M.
AU - Treur, J.
PY - 1997
Y1 - 1997
N2 - In this paper a compositional verification method for models of knowledge-based systems is introduced. Required properties of the system are formally verified by deriving them from assumptions that themselves are properties of sub-components, which in their turn may be derived from assumptions on sub-sub-components, and so on. The method is based on properties that are formalised in terms of temporal semantics; both static and dynamic properties are covered. The compositional verification method imposes structure on the verification process. By the possibility to focus at one level of abstraction (information and process hiding), compositional verification provides transparency and limits the complexity per level. Since verification proofs are structured in a compositional manner, they can be reused in case of modification of the system. The method is illustrated for a generic model for diagnostic reasoning.
AB - In this paper a compositional verification method for models of knowledge-based systems is introduced. Required properties of the system are formally verified by deriving them from assumptions that themselves are properties of sub-components, which in their turn may be derived from assumptions on sub-sub-components, and so on. The method is based on properties that are formalised in terms of temporal semantics; both static and dynamic properties are covered. The compositional verification method imposes structure on the verification process. By the possibility to focus at one level of abstraction (information and process hiding), compositional verification provides transparency and limits the complexity per level. Since verification proofs are structured in a compositional manner, they can be reused in case of modification of the system. The method is illustrated for a generic model for diagnostic reasoning.
KW - compositional verification
KW - knowledge-based systems
KW - diagnostic reasoning model
KW - formal compositional modelling
UR - http://www.scopus.com/inward/record.url?scp=84957871808&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/record.url?scp=84957871808&partnerID=8YFLogxK
U2 - 10.1007/BFb0026778
DO - 10.1007/BFb0026778
M3 - Conference contribution
SN - 3540635920
SN - 9783540635925
VL - 1319
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 65
EP - 80
BT - Knowledge Acquisition, Modeling and Management - 10th European Workshop, EKAW 1997, Proceedings
PB - Springer/Verlag
T2 - 10th European Workshop on Knowledge Acquisition, Modeling and Management, EKAW 1997
Y2 - 15 October 1997 through 18 October 1997
ER -