Testing Autonomous Systems Using Communicating Extended FSMs

Organisation:	University of Denver (USA)
Method:	Communicating extended finite-state machines LOTOS UML
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: http://ceur-ws.org/Vol-1514/paper1.pdf or from the CADP Web site in PDF or PostScript
Contact:	Anneliese Andrews Department of Computer Science University of Denver 2360 South Gaylord Street Denver, CO 80208 UNITED STATES Of AMERICA Phone: (303) -871-3374 Email: andrews@cs.du.edu
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page