Title :
Towards a verification of the rule-based expert system of the IBM SA for OS/390 Automation Manager
Author :
Sinz, Carsten ; Küchlin, Wolfgang ; Lumpp, Thomas
Author_Institution :
Wilhelm-Schickard-Inst. fur Inf., Tubingen Univ., Germany
Abstract :
We formally verify consistency aspects of the rule-based expert system of IBM´s System Automation software for IBM´s e-server zSeries. Starting with a formalization of the expert system in propositional dynamic logic (PDL), we are able to encode termination and determinism properties. To circumvent direct proofs in PDL or its extension ΔPDL, we further translate versions of the occurring decision problems to propositional logic, where we can apply advanced SAT and BDD techniques. In our experiments we revealed some inconsistencies, and after correcting them, we successfully verified a non-looping property for a part of the expert system
Keywords :
IBM computers; expert systems; formal logic; knowledge verification; program verification; theorem proving; ΔPDL; BDD techniques; IBM SA; IBM e-server zSeries; OS/390 Automation Manager; PDL; System Automation software; advanced SAT; consistency aspects; decision problems; determinism properties; direct proofs; expert system formalization; nonlooping property; propositional dynamic logic; propositional logic; rule-based expert system; rule-based expert system verification; termination; Application software; Automation; Binary decision diagrams; Business; Concurrent computing; Expert systems; Logic; Operating systems; Page description languages; Safety;
Conference_Titel :
Quality Software, 2001. Proceedings.Second Asia-Pacific Conference on
Conference_Location :
Hong Kong
Print_ISBN :
0-7695-1287-9
DOI :
10.1109/APAQS.2001.990042
