Database of Case Studies Achieved Using CADP

Testing Autonomous Systems Using Communicating Extended FSMs

Organisation: University of Denver (USA)

Method: Communicating extended finite-state machines

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

Domain: Embedded Systems.

Period: 2015

Size: 1346 states, 3658 transitions.

Description: Testing the interactions of autonomous systems with their environment, also called their world, is challenging due to both the complexity of the systems and the impredictability of their environment. This work proposes to leverage model-based testing techniques to the setting of autonomous systems, by deriving test cases from models of the environment.

The approach proceeds in three main steps. First the environment is modeled structurally (using an UML class diagram) and behaviourally (using communicating extended finite state machines). The behavioural model comprises a state machine per actor of the environment, plus a high level state machine describing the interactions of the actors. In a second step, several coverage critera are defined to control generation of test paths and partitioning of the input space for test data. Examples of the former are APSESCC (all possible serialized execution sequence coverage criterion) and RCC (rendezvous coverage criterion), and example of the latter are ACoC (all combinations coverage) and ECC (each choice coverage). Finally, concrete test cases are obtained by applying the different coverage criteria to the model. This step involves the computation of the composition of the different finite state machines. To measure the quality of the obtained test cases, the reachable state space of the model is computed by translation into LOTOS and subsequent usage of CADP.

The approach is illustrated on a tour-guide robot application in a shopping arcade, populated with passenger, mobile (cleaning machine) and fixed (information pannels) obstacles, and laser range finders (transmitting environment information to the robot). Each of these agents is modeled by a extended finite state machine (with two states). Applying the criteria APSESCC and ACoC yields more the 6 million test paths, but applying RCC and ECC yields the more reasonable number of 1736 test paths.

Conclusions: Regarding the LTS generation with CADP, [Andrews-Abdelgawad-Gario-15] states the following:
    CADP is scalable up to 10^13 nodes.

Publications: [Andrews-Abdelgawad-Gario-15] Anneliese Andrews, Mahmoud Abdelgawad, and Ahmed Gario. "Active World Model for Testing Autonomous Systems Using CEFSM". In Proceedings of the 12th Workshop on Model-Driven Engineering, Verification and Validation (MoDeVVa 2015), Ottawa, Canada, CEUR Workshop Proceedings, volume 1514, pp. 1-10, September, 2015.
Available on-line at:
or from the CADP Web site in PDF or PostScript
Anneliese Andrews
Department of Computer Science
University of Denver
2360 South Gaylord Street
Denver, CO 80208
Phone: (303) -871-3374

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

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

Back to the CADP case studies page