Database of Case Studies Achieved Using CADP

Abstraction and Analysis of Clinical Guidance Trees

Organisation: University of Stirling (SCOTLAND, UNITED KINGDOM)

Method: ADIT (Abstract Decision/Interactive Trees)

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:
or from our FTP site in PDF or PostScript

Ken Turner
Computing Science and Mathematics
University of Stirling
Stirling FK9 4LA
Tel: +44 1786 467 423
Fax: +44 1786 464 551

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page