André Pedro successfully defended his PhD thesis titled “Dynamic contracts for verification and enforcement of real-time systems properties” at UMinho in Braga

On the 5th of April of 2018, CISTER research André Pedro defended with success his PhD Thesis entitled “Dynamic contracts for verification and enforcement of real-time systems properties”. The evaluation committee included, among others, Professor Alan Burns from the University of York, United Kingdom, and Professor Simão Melo de Sousa, from University of Beira Interior, Portugal. The thesis defense took place in University of Minho.

André’s PhD Thesis addressed the topic of Runtime verification, an emerging discipline that investigates methods and tools to enable the verification of program properties during the execution of the application, and its application to real-time embedded systems development, whose frameworks are still lacking support for the verification of properties using explicit time where counting time (i.e., durations) and that are fundamental for the development process. Based on a restricted fragment of Metric temporal logic with durations, the thesis presents novel 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 fixed priority scheduler algorithms. A domain specific language is also proposed in order to describe such schedulability analysis problems in a more high-level way. Finally, we validate both approaches, the first using empirical scheduling scenarios, and the second using the use case of the lightweight autopilot system Px4/Ardupilot.

PHOTOS:
At CISTER's Facebook Page / At CISTER's Instagram Page