A carregar...
Publicação
Formalization and Runtime Verification of Invariants for Robotic Systems
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 638.11 KB | Adobe PDF |
Autores
Resumo(s)
Robotic systems are critical in today’s society, be it in manufacturing, medicine, or agriculture. A potential failure in a robot may have extraordinary costs, not only financial but can
also cost lives.
Current practices in robot testing are vast and involve methods like simulation, log checking,
or field testing. However, current practices often require human monitoring to determine the
correctness of a given behavior. Automating this analysis can not only relieve the burden from
a high-skilled engineer but also allow for massive parallel executions of tests that can detect
behavioral faults in the robots. These faults could otherwise not be found due to human error
or a lack of time.
I have developed a Domain Specific Language to specify the properties of robotic systems in
the Robot Operating System (ROS). Developer written specifications in this language compile
to a monitor ROS module that detects violations of those properties at runtime. I have used
this language to express the temporal and positional properties of robots using Linear Temporal
Logic as a basis for the language stipulation. I have also automated the monitoring of some
behavioral violations of robots in relation to their state or events during a simulation, resorting
to relations between the internal information of the system and the corresponding information
in the simulator.
To evaluate the developed work, I went through a list of documented ROS bugs and identified
some that happen at runtime. Using these bugs as a basis I specified the robot’s properties in
the developed language that should be capable of detecting an error, in order to test both the
expressiveness and the monitoring while running the system.
Descrição
Tese de mestrado, Engenharia Informática (Interação e Conhecimento), 2022, Universidade de Lisboa, Faculdade de Ciências
Palavras-chave
Robótica Linguagem de domínio Monitorização em tempo de execução Deteção de erros Teses de mestrado - 2023