Symbolic Analysis of Control Models for Autonomous Driving

Abstract

[ES] Se prevé que los vehículos sean completamente autónomos para 2040, lo que previsiblemente aportará beneficios considerables a la sociedad. Los vehículos autónomos (AV) dependen en gran medida de los avances en muchas de las técnicas y enfoques de la inteligencia artificial (IA), imponiendo nuevos desafíos en cuanto a garantizar su seguridad y confiabilidad. La necesidad de protocolos de control de vehículos autónomos cuya corrección pueda verificarse formalmente es primordial para la seguridad de todos, tanto en los centros urbanos como en carretera. Una situación representativa y de riesgo que ocurre con frecuencia durante la conducción sucede cuando dos o más vehículos encuentran una intersección. Para manejar este tipo de situaciones peligrosas, deben existir ciertos protocolos que puedan garantizar un entorno de conducción seguro, evitando bloqueos, inconsistencias en la comunicación y otros comportamientos indeseables.

El objetivo de este proyecto es analizar formalmente algunas propiedades críticas de un protocolo de control de vehículos autónomos conocido. Para lograr esto, primero se desarrollará un modelo formal del protocolo en el lenguaje de especificación de alto rendimiento Maude. A continuación, se llevará a cabo un análisis de la alcanzabilidad basado en narrowing para ayudar a descubrir cualquier fallo eventual en el modelo, de modo que se pueda obtener una nueva versión corregida del protocolo. Usando el comprobador de modelos de Maude, se pretende verificar las propiedades de seguridad y vivacidad del protocolo corregido, demostrando así que no se puede alcanzar ningún estado considerado inseguro y que el sistema está libre de inanición, es decir, que a ningún vehículo en la intersección se le niega perpetuamente el acceso.

[EN] Vehicles are predicted to be fully autonomous by 2040, which is expected to bring considerable benefits to society. Autonomous Vehicles (AV) heavily rely on advances in many Artificial Intelligence (AI) approaches and techniques, imposing new challenges to assure their safety and reliability. The need for autonomous vehicle control protocols whose correctness can be formally verified is paramount to ensure everyone¿s safety, both in urban centers and on the road. A representative, risky situation that frequently occurs while driving happens when two or more vehicles encounter an intersection. In order to handle these kinds of hazardous situations, some protocols must exist that can ensure a safe driving environment by preventing any deadlocks, communication inconsistencies, and/or other undesirable behaviors.

The aim of this project is to formally analyze some critical properties of a known autonomous vehicle control protocol. In order to achieve this, first a formal model of the control protocol is developed in the high-performance specification language Maude. A narrowing-based reachability analysis is then undertaken to help discover any eventual flaws in the protocol so that a new, corrected version of the model can be obtained. By using Maude¿s logical model checker (LMC), both safety and liveness properties of the corrected protocol will be eventually verified, proving that no states considered unsafe can be reached and that the system is starvation-free, i.e., that no vehicle at the intersection is perpetually denied to proceed.