|
| 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: |
CNUCE - CNR (Pisa, ITALY)
|
|---|---|
| Functionality: |
Specification and analysis of interactive applications
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Period: |
2000
|
| Description: |
An important part in the design of interactive software applications
is the user interface, which controls the dialogue with the users and
the presentation of the information. The goal is to obtain applications
able to support multiple users, in a flexible and effective way, while
they are performing their activities. To achieve this, it is necessary
to understand what tasks the users want to perform, to represent them
in order to better analyse their properties and relationships, and to
use this information in order to identify an effective user interface.
This motivated a growing research interest in the area of model-based
design methods (especially task models), which provide a useful basis
for the rigorous modelling and analysis of interactive applications.
ConcurTaskTrees is an easy-to-use notation for the specification of task models, which has been developed in order to overcome limitations of notations previously used for designing interactive applications. The ConcurTaskTrees Environment (CTTE), developed within the GUITARE ESPRIT Project, provides an integrated framework for designing user interfaces with the support of formal methods. CTTE offers the following main functionalities: task modelling, which enables the designer to obtain a ConcurTaskTrees specification of the application, describing in a structured, hierarchical way the different tasks involved and the temporal relationships among them; rapid prototyping, which allows to drive the development of a software prototype consistent with the requirements indicated in the ConcurTaskTrees model; ConcurTaskTrees-to-LOTOS transformation, which allows to translate a ConcurTaskTrees model into a LOTOS specification, each task being translated into a corresponding LOTOS process; property formalisation, which enables the designer to formulate the desired correctness properties of the task model by using a catalogue of parameterized templates associated to relevant property schemes; model-checking, which is performed using the CADP toolset on the LOTOS specification derived from the ConcurTaskTrees model. The use of CTTE is illustrated on a case-study in the field of Air Traffic Control. The environment has been successfully used to model and verify a system for air traffic control in the aerodrome area using data link communications. Several temporal logic properties, concerning interactions of the system with a single user (warning message for time-out expired) and with multiple users (mutual awareness, location-dependent coordination, mutual exclusive control) have been formulated in ACTL and verified using CADP. |
| Conclusions: |
The approach adopted in the CTTE environment has shown the usefulness
of the ConcurTaskTrees task modelling methodology in conjunction with
formal description techniques such as LOTOS and related model-checking
tools such as CADP in order to provide an integrated set of
functionalities for designing interactive applications. Further work
is planned to improve the specification of task model properties
and to allow the analysis of model-checking results (diagnostics)
directly in the ConcurTaskTrees model.
|
| Publications: |
[Paterno-Santoro-00]
Fabio Paternò and Carmen Santoro.
"Integrating Model Checking and HCI Tools to Help Designers
Verifying User Interface Properties".
In Ph. Palanque and F. Paternò, editors, Proceedings of the
7th International Workshop on Design, Specification and Verification
of Interactive Systems DSV-IS'2000 (Limerick, Ireland), Eurographics,
June 2000.
Available on-line from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Fabio Paternò CNUCE - CNR Via V. Alfieri 1 56010 Ghezzano, Pisa Italy Tel: +39 050 3153066 Fax: +39 050 3138091 E-mail: Fabio.Paterno@cnuce.cnr.it |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page