Modeling Robot Behavior with CCL

摘要

This paper presents the use of a Concurrent Communicating Lists (CCL) library in robot behavior modeling. CCL provides several software components, which allow the model to be built, simulated and formally verified. Due to the integration with the Robust library the CCL models can be deployed and executed on the actual hardware platforms. Besides the modeling robot behavior, the work also addresses the problem of modeling a robots environment. The CCL models can be verified either formally or by simulation. Since the use of formal methods is always associated with the state explosion problem, the work provides practical guidelines on how to deal with this problem using CCL.