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: Functional Verification 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. As software complexity evolves, so does the capacity to assure its
quality and correctness. Formal verification of software has been extensively used to prove the
correctness of safety critical systems in order to achieve high levels of reliability. A framework
that does precisely this is Frama-C. It takes as input ANSI-C programs annotated with properties in
ACSL and it tries to prove that the program is behaving according to the specification. 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)
annotate the software of an Arduino controller and (ii) fully verify it with Frama-C.