by Jeanine Souquières
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.
We report our experience on the specification development and verification of a real case study in the land transportation domain. It takes place in the context of the industrial CRISTAL ('Cellule de Recherche Industrielle en Systèmes de Transports Automatisés légers') and ANR (French National Research Agency) projects, which concern the development of a new type of self-service urban vehicle for the cities of tomorrow. The study is based on fleets of small electric vehicles specially designed for restricted access zones: historic city centres, airports, train stations or university campuses. These vehicles must be user-friendly and widely available, with features such as access control by smart card, simple manual control through a joystick, door-to-door services, automatic parking and recharging and a multimedia information terminal. Unfortunately, existing safety standards and guidelines are inadequate for assessing the safety and reliability of such new transportation systems, but in order to be approved and put into services, these vehicles do need to be certified.
With the development of this industrial case study, we address the importance of formal methods and their utility for highly practical applications. Our contribution mainly concerns methodological aspects for applying a component-based development approach using known results and tool supports: the model checker FDR2 and the B4Free proof tool. We show how to use the CSP||B framework to compositionally validate the specifications and prove the properties of component-based systems, with a precise verification process to ensure the consistency of a controlled machine and its generalization to a collection of controlled machines.
Case Study
A platoon is a set of autonomous vehicles that must move in convoy - ie following the path of the leader - through an intangible hooking mechanism. We consider each vehicle, named a Cristal, to be one agent in a multi-agent system. The Cristal driving system perceives information about its environment before passing acceleration instructions to its engine. In this context, the platooning problem is seen as a situated multi-agent system that evolves following the well-known Influence/Reaction model in which agents are described separately from the environment. The driving control includes both longitudinal control (maintaining an ideal distance between each vehicle) and lateral control (each vehicle should follow the track of its predecessor), as shown in Figure 1. Both controls can be studied independently.
The description of the case study involves detailing two architectural levels. We first consider a single Cristal composed of two parts, the vehicle and the driving system controlling the vehicle. Each part is itself built upon a B machine controlled by an associated CSP process. Once we identify the correct model for a single Cristal, we focus on the specification of a platoon as presented in Figure 2. We want the various Cristals to avoid 'going stale' when they move in a platoon; that is, we do not want communications in the convoy to deadlock. This might happen, for example, because a Cristal is waiting for information from its leader. In order to collect detailed information about the vehicle engine and its location, reflecting the separation of concerns within the platoon component, we allow the Cristal model to evolve. This evolution introduces new components and is achieved by adapters that connect these new components within the initial architecture.
Lessons Learned
This work highlights the main drawback of the CSP||B approach. At the interface between the two models, augmented B machines corresponding to CSP controllers are not automatically generated, and to perform this task manually requires a high level of expertise. In our opinion, the user should be able to conduct all the verification steps automatically; this could be a direction for future work.
Taking the case study further, we are currently studying new properties such as non-collision, non-unhooking and non-oscillation: which of these are expressible with CSP||B, and which are tractable and verifiable? This particular perspective is related to similar work by the authors of CSP||B dealing with another kind of multi-agent system. So far our use of CSP||B for the platooning model has led us to similar conclusions. This nonetheless raises the question of what impact the expression of more complex emerging properties does have on the model.
Further model development requires other refinement relations to be checked. It also includes evolution, in order to study what happens when a Cristal joins or leaves the platoon and which communication protocols must be obeyed for this to be achieved safely. We plan to take into account perturbations such as pedestrians or other vehicles.
With the evolution of the model, we illustrate a novel use of CSP||B theoretical results. Indeed, theorems about refinement or equivalences of CSP||B components are usually used to ease verification by allowing one to re-express a CSP controller into a simpler one. We used these results to show how to insert new behaviours by splitting up a controller/model compound without breaking previously verified properties.
Links:
http://tacos.loria.fr
http://www.projet-cristal.net
Please contact:
Jeanine Souquières
LORIA, Nancy-Université, France
E-mail: Jeanine.Souquieres
loria.fr
