Database of Research Tools Developed Using CADP

Modeling Robot Behavior with CCL

Organisation: AGH University of Science and Technology, Cracow (POLAND)

Functionality: Modeling and analysis of robot behavior.

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

Period: 2012

Description: The design and building of robots has gained increased interest in recent years. Robots have become accessible to a wide audience. The availability of sophisticated robotics platforms encourages researchers to seek new, efficient methods of modeling the control software for such constructions. This work proposes Concurrent Communicating List (CCL), a Clojure library supporting executable modeling of concurrent and distributed systems. It allows users to write a control program in a special Lisp-like CCL notation, run it step by step in a simulation mode, perform their formal verification or execute them like a regular computer program.

CCL notation is derived from process algebras and primarily focuses on behavior modeling. It defines operators and actions (as with the process algebras) which are used later to create more complex expressions forming a model specification. There are two types of communication: internal, between two different processes within the model, and external, between the model and the rest of the system (e.g., world model). Such a distinction provides modularization, since one module can be completely external to the other module. CCL, due to its close relationship with process algebras, gives the possibility to perform formal verification of the model. Some operations, such as deadlock finding or bisimulation checking, are supported directly by the CCL library. Others, such as temporal formula verification, are supported by exporting the model into the CADP toolbox. CCL is executable, which means that all the models can be freely simulated and executed. The approach is illustrated for modeling and analyzing the behaviour of an exploration robot.

Conclusions: The new CCL notation is supported by the CCL library, which offers several software components allowing for model building, model execution, model simulation and debugging, as well as formal analysis and verification of the model by connection to CADP. The CCL library integrates well with cljRobust and the Robust library, and thus all the models created and verified in the CCL notation can be easily executed on the actual hardware platforms. For modeling the boundary between the model of robot behavior and the external environment, the CCL library provides the CCL Sim simulation environment, which can imitate the outer environment, and allows users to write the model of the external world directly in the CCL notation.

Publications: [Kulakowski-Szmuc-12] Konrad Kulakowski and Tomasz Szmuc. "Modeling Robot Behavior with CCL". Proceedings of the 3rd International Conference on Simulation, Modeling, and Programming for Autonomous Robots SIMPAR'2012 (Tsukuba, Japan), Lecture Notes in Artificial Intelligence vol. 7628, pages 40-51. Springer Verlag, November 2012.
Available on-line at:

Konrad Kulakowski
Department of Applied Computer Science
AGH University of Science and Technology
Al. Mickiewicza 30
30-059 Krakow
Tel: +48 12 617 3408

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