Database of Case Studies Achieved Using CADP

Robot Teleoperation Architecture.

Organisation: University of Verona (ITALY)

Method: UML

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

Domain: Software Architectures.

Period: 2003

Size: about 100 lines of Basic LOTOS (specification)
about 20 lines (test purpose)

Description: The design, analysis, and construction of a complex system can be made conceptually more tractable by specifying the software architecture formally. The Unified Modeling Language (UML) allows to design object-oriented systems at different perspectives (abstraction levels), among which the architectural perspective. This perspective fixes certains design decisions such as naming of components (packages, classes) and connectors (associations, operations, inheritance relations). Several types of UML diagrams prove useful to express architectural requirements: package diagrams partition an architecture into separate layers, class diagrams represent static structure requirements, and interaction or state diagrams represent dynamic properties of the components and connectors present in the architecture.

Architectural unit testing encompasses two activities: testing of architectural unit models against their functional requirements, and design of testers for architectural units. The methodology adopted for architectural unit testing consists of the following ingredients:
  • Description of the system architecture by using (a subset of) UML class diagrams and state diagrams for specifying the static structure and the dynamic requirements on architectural units, respectively. State diagrams must obey certain restrictions (e.g., all edges that enter or leave a composite state must have their ending at the composite state contour rather than at some inner state) intended to improve their structure and to facilitate their subsequent manipulation.

  • Translation of the UML state diagrams into Basic LOTOS. Each state in a diagram is translated into a LOTOS process, which enables hierarchical description of composite states using LOTOS subprocesses. Transitions going out of states are modelled in LOTOS by using the action prefix, choice, and stop operators. Transitions corresponding to the succession of composite states are modelled using the LOTOS enabling operator, and transitions going out from inner states of a composite state are represented using the LOTOS disabling operator. The resulting LOTOS models are then translated into (Input/Output) Labelled Transition Systems (IOLTSs) by using the CAESAR compiler of CADP.

  • Test purposes corresponding to functional requirements are encoded in Basic LOTOS, and subsequently translated into IOLTSs using CAESAR. Then, from the LOTOS specification of an architectural unit and a test purpose, the corresponding test cases are generated by using the TGV tool of CADP.
This methodology was applied for testing a software architecture dedicated to robot teleoperation. The architecture consists of three layers: the planning layer manages real-time tasks defined using artificial intelligence techniques, to provide a deliberative component; the control layer provides the previous layer with functionalities that implement user interaction or are independent from hardware; and the execution layer implements the more concrete classes, that interact with the hardware subsystem. The case-study focused on the control layer, which contains four packages: CommandInterpreter, MotionControl&Manipulation, Compensation&Filtering, and Vision&Perception. The unit chosen for testing was that represented by the class TrajectoryGen of the package MotionControl&Manipulation. After translating in Basic LOTOS the state diagram of this class, a test purpose was written in LOTOS, corresponding to the requirement that the TrajectoryGen unit should always output trajectories which prevent collisions with still objects, assuming no new object is detected during trajectory computation. From these inputs, the TGV tool generated a succinct test case (9 states), obtained by giving priority to the actions of the test purpose w.r.t. those of the specification.

Conclusions: A formal testing methodology was proposed and experimented on a non-trivial example of software architecture, allowing to assess testability of functional requirements as well as to generate architectural models of unit testers at early design stages. The methodology is based upon object-oriented modeling with a clean IOLTS semantics obtained by translating UML state diagrams into LOTOS, which allows the subsequent use of the CADP tools for compilation and automated test generation.

Publications: [Scollo-Zecchini-03] Giuseppe Scollo and Silvia Zecchini. "Architectural Unit Testing in a Robot Teleoperation Case Study". Research Report RR 12/2003, University of Verona, October 2003.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Scollo-Zecchini-05] Giuseppe Scollo and Silvia Zecchini. "Architectural Unit Testing". In Proceedings of the International Workshop on Model Based Testing MBT'2004 (Barcelona, Spain), Electronic Notes in Theoretical Computer Science vol. 111, 2005.
Available on-line from the CADP Web site in PDF or PostScript
Dr. Giuseppe Scollo
Associate Professor
Department of Computer Science
University of Verona
Ca'Vignal 2 - Strada le Grazie 15
37134 Verona
Tel: 045 802 7940
Fax: 045 802 7068

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

Last modified: Thu Feb 11 12:22:04 2021.

Back to the CADP case studies page