“How can we model autonomous cars in the most general way and establish the absence of catastrophic events? How to preserve such safety properties under extensions of the model?" This question marked the beginning of a fruitful partnership with SystemX on projects like SVR and now 3SA involving industrial partners such as transdev, Renault and PSA.
Previous work on the process algebra CSP in the Higher-order Logic framework Isabelle/HOL inspired us to reuse our interactive proof environment Isabelle/HOL-CSP developed for studying process architectures such as rings or networks, for this purpose. HOL-CSP is centred around events parameterised by an arbitrary HOL-type and non-deterministic processes with internal states. Thus, HOL-CSP processes can directly reuse the rich Isabelle/HOL libraries containing real-number analysis, vector-space algebra and other mathematical machinery. Moreover, parametric polymorphism of HOL is used to make the process states extensible in an object-oriented manner, thus relating processes by a form of inheritance and leading to some form of “open world”-assumption.
In Isabelle/HOL-CSP, one can model different types of actors, i.e, cars, pedestrians, traffic lights, as processes that communicate their internal physical state (position, speed, current acceleration, potential accelerations, etc.). State changes of actors are only allowed according to the laws of Newtonian mechanics. This model gives rise to the definition of a non-deterministic function, the driving strategy, that chooses from the global state of all actors — the scene — a particular acceleration from the set of potential accelerations for a given actor. The chosen acceleration vector is applied to the actor state during a non-deterministically chosen, infinitesimal time interval, which yields its next state.
Our partners asked us to apply our approach for cyber-physical systems to a particular driving strategy well-known in the literature and proven safe by paper-and-pencil proofs: the “Responsibility Sensitive Safety” (RSS) proposed by Shaliv-Shwartz, Shaman and Shashua. A formalisation of RSS in our framework was straightforward; our formal proof revealed that the informal safety proof of RSS involved flawed arguments. Using another line of arguments, our machine-checked proof is still of fairly modest size (450 lines in Isabelle/Isar). Moreover, we developed a generalisation to a scenario with multiple cars on a lane, and an improvement of the strategy called RSS+ with shorter safety distances that is still collision free and therefore safe in our sense. Additionally, it was possible to extract abstract test cases from the proof, which essentially represent intervals between tipping points of acceleration and braking-curves, and that may serve for a test-bench of system-integration tests.
Currently, our industrial partners (Stellantis, CEA, LNE and IRT SystemX) decided to continue our collaboration in the context of the SystemX/3SA project and of an IRT SystemX exploration project named “A formal approach to model and process the properties of hybrid systems” piloted by Paolo Crisafulli. In these activities, we address the problem of multi-dimensional collision avoidance strategies and the relaxation of certain hypothesis underlying the RSS model. Overall, the project volume comprises meanwhile about 215 kEUR, including the hiring of a postdoc for one year and the association of 1 Phd project concerning the foundations of HOL-CSP and its applications.
Safouan TAHA & Burkhart WOLFF
Links: Technical report, Invited talk at Exeter University video