Database of Case Studies Achieved Using CADP

Rigorous Development of Prompting Dialogs

Organisation: University of Stirling (Scotland, UK)

Method: CRESS

Tools used: CRESS
CADP (Construction and Analysis of Distributed Processes)

Domain: Human-Computer Interaction.

Period: 2011

Size: 561,770 states and 3,252,002 transitions.

Description: Cognitive impairment is widespread and has various causes including dementia, stroke, traumatic injury, learning difficulties and mental illness. People with cognitive impairment can have problems initiating, planning, sequencing, attending and remembering. Severe cognitive impairment can make it impossible without support to perform routine activities of daily living such as food preparation, dressing, laundering, and self-care. Technological support for people with cognitive impairment is therefore highly desirable. Assistive technology for cognition has been shown to help people with dementia, traumatic brain injury and cerebrovascular accident. Several reminding devices have been developed to help people with daily tasks. Recent research work focuses on micro-prompting (or sequencing) systems that guide users step-by-step through a given activity by simulating the verbal prompting provided by carers.

Prompting for even relatively ordinary tasks requires careful design of complex dialogues. These are typically prepared by care professionals or family members. Errors in prompting dialogues are undesirable as they are likely to confuse a user who is already struggling to complete a task. Incorrect dialogues can also raise safety concerns. No established procedure is currently available for ensuring that the dialogues used in prompting devices are error-free. This work considers the GUIDE (General User Interface for Disorders of Execution) prompting system, and aims at improving it in several respects: simplifying the design of prompting dialogues; automating the checking of dialogues for technical errors in syntax and semantics; and automating the translation of dialogue designs into a form allowing their ready deployment.

The methodology proposed consists of the following ingredients. Prompting dialogues are described formally using the CRESS (Communication Representation Employing Systematic Specification) graphical notation, which is independent of the application domain and target languages. Then, CRESS diagrams are automatically translated in LOTOS for validation purposes. Correctness properties of prompting dialogues are specified in the CLOVE language, then translated automatically into regular alternation-free mu-calculus formulas, and verified using the EVALUATOR model checker of CADP. Finally, implementations of the CRESS dialogue descriptions in VoiceXML are generated automatically. The whole approach is successfully illustrated on four significant dialogues for supporting cognitive impaired people: blood sugar testing, hand washing, donning an artificial limb, and making a strawberry smoothie.

Conclusions: The proposed methodology for handling prompting dialogues improves GUIDE in several respects: the design of prompting dialogues was simplified using CRESS' graphical notation, which makes the flow in dialogues much clearer and facilitates dialogues modification; the checking of dialogues for syntactic and semantic errors was achieved by automatic translation into LOTOS specifications, which are validated automatically using CADP; finally, dialogue designs were translated automatically into a VoiceXML platform, which allows their ready deployment. The methodology is generic in that it can be used for rigorous design in many application areas (e.g., response services, telephony services, web services, grid services, device services, etc.).

Publications: [Turner-Gillespie-McMichael-11] Kenneth J. Turner, Alex M. Gillespie, and Lynne J. McMichael. "Rigorous Development of Prompting Dialogues". Biomedical Informatics, 44(4):713-727, September 2011.
Available on-line at:
or from the CADP Web site in PDF or PostScript
Prof. Kenneth J. 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: Thu Feb 11 12:22:03 2021.

Back to the CADP case studies page