University of Stirling (Scotland, UK)
CADP (Construction and Analysis of Distributed Processes)
561,770 states and 3,252,002 transitions.
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.
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,
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: http://www.cs.stir.ac.uk/~kjt/research/pdf/rig-dial.pdf
or from our FTP 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: http://cadp.inria.fr/case-studies|