|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 the CADP Web 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: [email protected] |
| Further remarks: | This application, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page