Database of Research Tools Developed Using CADP

ConcurTaskTrees Environment

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
Fabio Paternò
Via V. Alfieri 1
56010 Ghezzano, Pisa
Tel: +39 050 3153066
Fax: +39 050 3138091

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:23:11 2021.

Back to the CADP research tools page