Ensuring the Reliability of an Autonomous Vehicle: a Formal Approach based on Component Interaction Protocols

In automotive applications, several components, offering different services, can be composed in order to handle one specific task (autonomous driving for example). Nevertheless, component composition is not straightforward and is subject to the occurrence of bugs resulting from components or services incompatibilities for instance. Hence, bugs detection in component-based systems at the design level is very important, particularly, when the developed system concerns automotive applications supporting critical services. In this paper, we propose a formal approach for modeling and verifying the reliability of an autonomous vehicle system, communicating continuously with off-road infrastructure. We focus on components offering critical services with hard time constraint defining the delay of their availability. We propose to verify whether a set of components, when composed according to the system architecture specified with SysML models, achieve their tasks by respecting their interaction protocols and their time constraints.