|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: http://link.springer.com/chapter/10.1007%2F978-3-642-34327-8_7 |
| Contact: | Konrad Kulakowski Department of Applied Computer Science AGH University of Science and Technology Al. Mickiewicza 30 30-059 Krakow Poland Tel: +48 12 617 3408 Email: [email protected] |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page