A Component-Based Approach for the Specification and Verification of Safety-Critical Software: Application to a Platoon of Vehicles

The platoon of vehicles is a mixture of distributed and embedded systems. The former are usually hard to understand and debug as they can exhibit obscure behaviours. The latter must satisfy safety/security/confidence requirements, both when standing alone and when composed together. To address these problems, we propose a component-based development approach using the CSP||B framework of well-established formal methods: B for the development of provably correct software, and CSP for Communicating Sequential Processes.