Database of Case Studies Achieved Using CADP

Formal Verification in the Framework of an Interactor Model.

Organisation: Department of Computer Science, Queen Mary and Westfield College, University of London (UNITED KINGDOM)

Method: LOTOS

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

Domain: Human-Computer Interaction.

Period: 1996-1998.

Size: n/a

Description: The abstraction-display-controller (ADC) interactor model is an architectural construct for modelling human-computer interface software. Interactors are basic communication entities that cooperate with each other in order to manage the dialogue between a user and an application. Interactors are modelled as LOTOS processes that interact with each other (and possibly with the user) by synchronizing and communicating data via LOTOS gates.

In [Markopoulos-Rowson-Johnson-96] the ADC model is illustrated by the formal treatment of modelling the dialogue between the user and the application. The abstract specification of the interface as an interactor is refined by a modular decomposition into a network of interactors that implements it. The CAESAR and ALDEBARAN tools are used for model-checking several response (syntactic feedback) properties of the system.

In [Markopoulos-97] an extensive study of the ADC model is presented. A wide spectrum of properties of ADC interactors (result predictability, observability), of dialogue (deadlock freedom, completeness, action reachability), and of tasks (task conformance) are formally defined. The verification of these properties on various LOTOS specifications of ADC interactors is experimented using specialized model-checking tools such as CAESAR/ALDEBARAN and JACK.

Conclusion: As outlined in [Markopoulos-Johnson-Rowson-98], interactor models such as ADC offer a practical approach to the development of interactive systems. Moreover, the ADC interactor model provides a mapping of concepts of the HCI domain into LOTOS language elements, thus allowing to apply in the framework of interactive software design all the formal verification techniques and tools available for LOTOS.

Publications: [Markopoulos-Rowson-Johnson-96] Panos Markopoulos and Jon Rowson and Peter Johnson. "Dialogue Modelling in the Framework of an Interactor Model". In: Proceedings of the 3rd International Workshop on Design, Specification, and Verification of Interactive Systems DSV-IS '96 (Namur, Belgium), June 1996.
Available on-line at: ftp://ftp.dcs.qmw.ac.uk/pub/hci/publications/96-MarkopoulosP-1.ps.gz
or also from our FTP site in PDF or PostScript

[Markopoulos-97] Panos Markopoulos. "A Compositional Model for the Formal Specification of User Interfaces". PhD thesis, Queen Mary and Westfield College, University of London (UK), March 1997.
Available on-line at: http://www.idemployee.id.tue.nl/p.markopoulos/downloadablePapers/PhDThesisPanosMarkopoulos.pdf

[Markopoulos-Johnson-Rowson-98] Panos Markopoulos and Peter Johnson and Jon Rowson. "Formal Architectural Abstractions for Interactive Software". International Journal on Human-Computer Studies 49(5), December 1998.
Available on-line at: http://www.idemployee.id.tue.nl/p.markopoulos/downloadablePapers/ijhcs.pdf
Contact:
Panos Markopoulos
Assistant Professor
User Centred Engineering
Industrial Design, TU/e
MG 2.38, P.O. Box 513
Den Dolech 2
5600 MB Eindhoven
The Netherlands
Tel: +31 40 247 5247
Fax: +31 40 247 5376
E-mail: P.Markopoulos@tue.nl



Further remarks: This application, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


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


Back to the CADP case studies page