Towards validating a platoon of cristal vehicles using CSP∥B

Abstract

The so-called platooning problem consists in making autonomous vehicles move in a convoy. It crosses several domains: distributed systems, embedded systems, multi-agent systems and critical systems. We thus propose to use the combination named CSP||B of two well-known formal methods to assess and verify properties of this complex system. To that end we make use of previous theoretical results on CSP||B. We also illustrate how this methodology spans the multiple composition levels of the resulting model. © 2008 Springer-Verlag Berlin Heidelberg.