Organisation: |
University of Stirling (SCOTLAND, UNITED KINGDOM)
|
---|---|
Method: |
ADIT (Abstract Decision/Interactive Trees)
LOTOS |
Tools used: |
MUSTARD (Multiple-Use Scenario Testing and Refusal Description)
PCL (Parameter Constraint Language) CADP (Construction and Analysis of Distributed Processes) |
Domain: |
Health Care.
|
Period: |
2008
|
Size: |
430 lines of LOTOS (10 processes) for the
benign prostatic hyperplasia tree
|
Description: |
Clinical Guidance Trees (CGTs) are an extension of decision
trees adapted to clinical practice. Contrary to conventional medical
decision trees, CGTs are oriented towards use by non-specialists and
provide support for interactive exploration. Automated support for CGT
manipulation (mainly, a CGT viewer) was developed in the framework of
a project focused on several medical conditions: benign prostatic
hyperplasia (swelling of the prostate), hypertension (high blood
pressure), influenza, and menorrhagia (excessive bleeding during
periods). The CGT viewer reads decision trees in a textual notation
(with keywords and layout) and provides various functionalities:
explanation, exploration, analysis, recommendation, summarizing an
exploratory session and recording user's choices for statistical
analysis.
Due to their interactive nature, CGTs are prone to a class of errors that do not arise in conventional decision trees. Therefore, a new design and analysis approach is needed in order to detect such errors in CGTs. Formal methods are a natural candidate for supporting this approach, because they can effectively describe and analyze the exploration of a tree of behaviours. A new notation and methodology for defining CGTs, named ADIT (Abstract Decision/Interactive Trees) was proposed. ADIT allows to start with an initial concept and to refine it into a decision tree, by clearly identifying the structure and contents of the tree. As in other forms of decision trees, ADIT defines the chance, decision, and terminal tree nodes, and also a question node allowing to capture user input during the tree exploration. Finally, a value definition allows to associate content (in the form of attributes of various kinds) with a node. An example of CGT tree defined using ADIT can be found in [Turner-08]. This example shows a fragment of the decision tree for benign prostatic hyperplasia, the treatment of which can follow two branches: either transurethral resection of the prostate, which may have consequences on the sexual activity of the patient, or phytotherapy, which is based on herbs or plant extracts. ADIT descriptions are automatically translated into LOTOS for formal analysis. The translation of a CGT is an abstraction of what the user sees when exploring it. Various abstract data types were defined in LOTOS for the ADIT library, including real numbers defined using a sign-whole-fraction representation, and maps associating values to the CGT variables. Tree expressions are translated into LOTOS processes, which take a variable map and produce a variable map. These processes behave almost like functions but can have sequences, conditions, and side-effects. Basically, each tree node is translated into a LOTOS process, which encodes the actions performed by the user when exploring the CGT. CGTs may be subject to several kinds of design errors, which must be detected and corrected: syntactic errors (badly formed trees), static semantic errors (type checking and variable binding), path errors (unsuccessful tree exploration), numeric errors (incorrect calculations), and explanation errors (incorrect feedback given to the user). The current study focuses on path errors, which are related to the interactive nature of CGTs and cannot be analyses using existing methods for classical decision trees. Starting from the LOTOS specifications automatically generated from the ADIT tree descriptions of of four health care CGTs (benign prostatic hyperplasia, influenza, hypertension, and menorrhagia), the following analyses were carried out on the underlying state spaces: absence of deadlocks (which would cause some leaf nodes to become unreachable), absence of livelocks (infinite loops causing a question to be asked repeatedly), and general properties (e.g., existence of a certain branch in the tree after some decision has been taken by the user). General properties were checked using CADP, either by means of LOTOS test processes, or by means of temporal logic formulas written in the XTL language. Several categories of errors have been found in the four health care studies: structural errors (inability to explore certain subtrees), initialisation errors (variables initialized in the wrong order), macro errors (macros used in numeric calculations and not only in text values), condition errors (wrong evaluation results of condition expressions), missing range checks (meaningless values for certain variables due to unspecified ranges), and incorrect range checks (input values insufficiently checked for validity, leading to incorrect advice in the end). |
Conclusions: |
Several important goals were achieved: definition of ADIT, an abstract
notation for CGTs, which allows to separate the structure from the
content; the translation of ADIT into LOTOS, which provided a rigorous
semantics for CGTs; implementation of an automated translator from ADIT
to the CGT viewer for visual exploration of CGTs; and the successful
application of the approach on four health care studies.
The ADIT notation and the associated methodology can be also used in other domains, such as data mining, finance, and risk assessment. Due to the connection to LOTOS and verification tools like CADP, this would provide powerful analysis capabilities to be applied in these domains. |
Publications: |
[Turner-08]
Kenneth J. Turner.
"Abstraction and Analysis of Clinical Guidance Trees". In Journal of Biomedical Informatics, 2008.
Available on-line at: http://www.cs.stir.ac.uk/~kjt/research/pdf/abs-cgt.pdf or from the CADP Web site in PDF or PostScript |
Contact: | Ken Turner Computing Science and Mathematics University of Stirling Stirling FK9 4LA Scotland Tel: +44 1786 467 423 Fax: +44 1786 464 551 Email: [email protected]. |
Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |