loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Second Asia-Pacific Conference on Quality Software (APAQS'01)
Towards a Verification of the Rule-Based Expert System of the IBM SA for OS/390 Automation Manager
Hong Kong
December 10-December 11
ISBN: 0-7695-1287-9
ASCII Text
x 
 
C. Sinz, W. Küchlin, T. Lumpp, "Towards a Verification of the Rule-Based Expert System of the IBM SA for OS/390 Automation Manager," Asia-Pacific Conference on Quality Software, pp. 0367, Second Asia-Pacific Conference on Quality Software (APAQS'01), 2001.
 
 
BibTex
x
 
@article{ 10.1109/APAQS.2001.990042,
author = {C. Sinz and W. Küchlin and T. Lumpp},
title = {Towards a Verification of the Rule-Based Expert System of the IBM SA for OS/390 Automation Manager},
journal ={Asia-Pacific Conference on Quality Software},
volume = {0},
year = {2001},
isbn = {0-7695-1287-9},
pages = {0367},
doi = {http://doi.ieeecomputersociety.org/10.1109/APAQS.2001.990042},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Asia-Pacific Conference on Quality Software
TI - Towards a Verification of the Rule-Based Expert System of the IBM SA for OS/390 Automation Manager
SN - 0-7695-1287-9
SP
EP
A1 - C. Sinz,
A1 - W. Küchlin,
A1 - T. Lumpp,
PY - 2001
VL - 0
JA - Asia-Pacific Conference on Quality Software
ER -
 
C. Sinz, University of T?bingen, WSI
W. Küchlin, University of T?bingen, WSI
T. Lumpp, IBM Germany Development
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 \Delta, 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 could reveal some inconsistencies and, after correcting them, we successfully verified a non-looping property for a part of the expert system.
Citation:
C. Sinz, W. Küchlin, T. Lumpp, "Towards a Verification of the Rule-Based Expert System of the IBM SA for OS/390 Automation Manager," apaqs, pp.0367, Second Asia-Pacific Conference on Quality Software (APAQS'01), 2001
Usage of this product signifies your acceptance of the Terms of Use.