SAT 2004 START ConferenceManager    


Verifying the On-Line Help System of SIEMENS Magnetic Resonance Tomographs using SAT

Carsten Sinz and Wolfgang Küchlin

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

[NOTE: THIS PAPER IS CONFIDENTIAL AND IS UNDER REVIEW FOR PATENT] Large-scale medical systems---for example magnetic resonance tomographs---are manufactured with a steadily growing number of product options. Different basic models can be equipped with large numbers of different supplementary equipment like (gradient) coils, amplifiers, magnets or imaging devices. The necessary service and maintenance procedures, which may be different for each of the many product instances, are growing accordingly in quantity and complexity. Therefore, instead of one common on-line service handbook for all medical devices, SIEMENS fragments the on-line documentation into small (help) packages, out of which a suitable subset is selected for each individual product instance. Selection of the packages is controlled by Boolean formulae (encoded in XML). To check whether the existing set of help packages is sufficient for all possible devices and service cases, we developed the HelpChecker tool. HelpChecker uses both SAT- and BDD-based methods to check the consistency and completeness of the on-line documentation and to generate small (counter-)examples for possibly emerging errors.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com