Doctoral Thesis Defense - André de Matos Pedro

Tuesday, April 10, 2018, 10:00am

Title: Dynamic contracts for verification and enforcement of real-time systems properties

Abstract: Runtime verication is an emerging discipline that investigates methods and tools to enable the verication of program properties during the execution of the application. The goal is to complement static analysis approaches, in particular when static verication leads to the explosion of states. Non-functional properties, such as the ones present in real-time systems are an ideal target for this kind of verication methodology, as are usually out of the range of the power and expressiveness of classic static analyses.

Current real-time embedded systems development frameworks lack support for the verication of properties using explicit time where counting time (i.e., durations) may play an important role in the development process. Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of Metric temporal logic with durations (MTL-R), we will present the synthesis mechanisms 1) for target systems as runtime monitors and 2) for SMT solvers as a way to get, respectively, a verdict at runtime and a schedulability problem to be solved before execution. The later is able to solve partially the schedulability analysis for periodic resource models and xed priority scheduler algorithms.

A domain specic language is also proposed in order to describe such schedulability analysis problems in a more high level way. Finally, we validate both approaches, the rst using empirical scheduling scenarios, and the second using the use case of the lightweight autopilot system Px4/Ardupilot.

Supervisors: Jorge Sousa Pinto and Luís Miguel Pinho

Jury: - Rector of the University of Minho

        - Doctor Fernando Manuel Augusto da Silva, Full Professor - Departamento de Ciência de Computadores da Faculdade de Ciências da Universidade do Porto

        - Doctor Simão Melo de Sousa, Associate Professor with Habilitation - Departamento de Informática da Faculdade de Engenharia da Universidade da Beira Interior

        - Doctor Maria João Gomes Frade, Assistant Professor - Departamento de Informática da Escola de Engenharia da Universidade do Minho

        - Doctor Luís Miguel Pinho, Coordinating Professor - Departamento de Engenharia Informática do Instituto Superior de Engenharia do Porto do Instituto Politécnico do Porto

        - Doctor Alan Burns, Full Professor da University of York, Reino Unido

Location: Auditorium B2 - Campus de Gualtar - Universidade do Minho - Braga