Propostas para Dissertação

Mestrados no Departamento de Informática

Consultar ficha completa de uma proposta de dissertação

proponente: Alcino Cunha e Cláudio Lourenço
instituição/empresa: Universidade do Minho
tema/título: Model Checking of Robotic Arduino Controllers
área científica: Software Engineering
local: Braga
curso de mestrado: Mestrado Integrado em Engenharia Informática
Programmable logic controllers (PLCs) are often used in robotic safety controllers, since their
robustness and simplicity renders them easily certifiable. However, with the continuous expansion
of robotics to more unstructured environments and a closer human interaction, modern robotic
systems are expected to be highly configurable and adaptive, which requires flexible modes of
operation. The limited processing power of PLCs hinders their applicability in such systems, which
has triggered a paradigm shift towards software safety controllers written in higher-level
programming languages deployed in microprocessors such as Arduinos. However, this shift complicates safety certification processes, since software certification is
still a challenging task. There are two approaches that are widely used to improve software quality
and correctness: software testing and formal verification of software. While the first cannot prove
the absence of errors, the second is very time consuming, since it requires the code to be
annotated with contracts and loop invariants. Bounded model checking of software lies in the middle
of this spectrum, and it can automatically detect safety errors and violations of user inserted
assertions. Even though it cannot prove the absence of errors, the technique is useful since it
able to detect errors in the code at no extra cost. Although software used in Arduino controllers is more complex than PLCs, it is still very
restrictive when compared to standard software systems. The goal of this thesis is thus to (i)
develop a technique to automatically apply bounded model checking of software to an Arduino robotic
controller and (ii) apply the developed technique to the Arduino controller standard library.