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

fYear

2001

fDate

2001

Firstpage

367

Lastpage

374

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Quality Software, 2001. Proceedings.Second Asia-Pacific Conference on

Conference_Location

Hong Kong

Print_ISBN

0-7695-1287-9

Type

conf

DOI

10.1109/APAQS.2001.990042

Filename

990042