Summary

Large-scale medical systems - like magnetic resonance tomographs - are manufactured with a steadily growing number of product options. Different model lines can be equipped with large numbers of supplementary equipment options like (gradient) coils, amplifiers, magnets or imaging devices. The diversity in service and maintenance procedures, which may be different for each of the many product instances, grows accordingly.

Therefore, instead of having one common on-line service handbook for all medical devices, SIEMENS parcels out the on-line documentation into small (help) packages, out of which a suitable subset is selected for each individual product instance. Selection of packages is controlled by XML terms. To check whether the existing set of help packages is sufficient for all possible devices and service cases, we developed the Help-Checker-Tool (HCT). HCT translates XML input into Boolean logic formulae and employs both SAT- and BDD-based methods to check consistency and completeness of the on-line documentation.

To explain its reasoning and to facilitate error correction, it generates small (counter-)examples for cases where verification conditions are violated. We expect that a wide range of cross-checks between XML documents can be handled in a similar manner using our techniques.

Detailed Information:

SIEMENS Medical Solutions uses XML terms to describe the totality of their magnetic resonance (MR) tomograph range of products. This is done using a tree-like structure of Item and Type Nodes. Type Nodes are employed to reflect the hierarchical product structure, whereas Item Nodes represent possible configuration options with common functionality. Moreover, item nodes may be labeled by Constraints that have to be fulfilled in order to make the Item a valid product option. Fig. 1 shows a simplified example of an MR product structure.

Fig. 1: Product Structure of Magnetic Resonance Tomographs (Simplified Example).

The cornerstones of the HCT project are as follows:

• The (on-line) product documentation is broken down into small Help Packages.
• Assignment of Help Packages to MR System Configurations is controlled by Boolean logic formulae encoded in XML.
• Two questions to answer in order to obtain correct handbooks:
  1. Consistency: Are there any help package overlaps?
  2. Completeness: Are there any missing help packages?

To answer these questions we use different automatic reasoning techniqes. First, we encode the problems as logical satisfiability problems. We then are able to apply advanced SAT solvers and Binary Decision Diagrams (BDDs) to check consistency and completeness of the product documentation. The methodology is schematically depicted in Fig. 2.

Fig. 2: Systematics of SAT Encoding and Consistency Checks

HCT is part of a larger authoring system developed by Tanner AG, Lindau, Germany and SIEMENS Medical Solutions, Erlangen, Germany.

Wolfgang Küchlin:

SIEMENS Medical Solutions

Tanner AG