Detection of dynamic execution errors in IBM system automation's rule-based expert system

摘要

We formally verify aspects of the rule-based expert system of IBM's system automation software for IBM's zSeries mainframes. Starting with a formalization of the expert system in propositional dynamic logic (PDL), we encode termination and determinism properties in PDL and its extension ΔPDL. We then translate our decision problems to propositional logic and apply advanced SAT techniques for automated proofs. In order to locate real program bugs for each failed proof attempt, we apply extra formalization steps and represent propositional error formulae in concise normal form as binary decision diagrams. In our experiments, we revealed residual non-termination bugs in a tested program version close to shipment, and, after correcting them, we formally verified the absence of this class of bugs in the production code.