Monitoring road traffic rules with spatio-temporal properties

Abstract

As technology evolves our world becomes filled with ubiquitous systems. Yet, at some point, technology has to be tamed because safety-critical systems, if not meticulously designed and validated, may represent a threat to us and to our environment. This work aims at the verification and validation of safety-critical systems, such as autonomous driving systems, using runtime monitoring methods. We studied the monitoring of spatio-temporal properties which cope with the evolution of a space model during the flow of time, and an automatic monitor generation mechanism. The situation presented as a case study in this dissertation considers an autonomous driving system on an urban environment, where our purpose is to monitor safety-margins between vehicles, the road, and the surrounding environment. A set of informally written requirements for the system were formalized in a spatio-temporal logic. This allows for these expressions to be transformed into monitors, programs, that are able to observe the behaviours considering space and time. Finally, a tool was implemented which applies the monitoring method developed throughout this dissertation given a sequence of events captured by an autonomous driving simulation software. In conclusion, we hope to be taking a step forward to making driving a more automated, pleasant, and safer experience through the verification and validation of autonomous driving systems.

À medida que a tecnologia evolui o nosso mundo fica cada vez mais repleto de sistemas ubíquos. No entanto, a certo ponto é preciso domar esta tecnologia porque se sistemas críticos de segurança não forem meticulosamente desenhados e validados poderão representar perigo para nós ou para o nosso ambiente. Este trabalho consiste na verificação e validação de sistemas críticos, por exemplo, sistemas de condução autónoma, usando métodos de monitorização em tempo de execução. Estuda-se a monitorização de propriedades espácio-temporais que lidam com a evolução do espaço ao longo do tempo e a geração de monitores de forma automática. O cenário apresentado como caso de estudo nesta dissertação considera um sistema de condução autónoma num ambiente urbano onde o objetivo é monitorizar as margens de segurança entre os veículos, a estrada e o ambiente que os rodeia. Foram escritos vários requisitos em linguagem natural e depois formalizados numa logica espácio-temporal. Isto permite que estas expressões possam dar lugar a monitores, programas, que são capazes de observar os comportamentos de espaço e tempo. Por fim foi desenhada uma ferramenta que aplica o método desenvolvido nesta tese e integrada a ferramenta com o software de simulação de condução autónoma. Para concluir, esperamos estar a dar um passo em frente para tornar a condução de veículos uma experiência mais automatizada, prazerosa e segura através da verificação e validação de sistemas de condução autónoma.