Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:PROSA: A Foundation for Verified Schedulability Analysis
Speaker:Felipe Augusto Queiroz de Cerqueira
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Proposal
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Monday, 10 September 2018
Duration:60 Minutes
Real-time systems comprise the class of systems that are subject to physical
timing constraints, i.e., in order to be considered sound, they must be checked
for both functional and temporal correctness. Regarding the latter, apart from
choosing appropriate scheduling policies to be applied at runtime, system
designers must confirm that the temporal requirements of the system are
met by using methods known as schedulability analyses.

As opposed to the more measurement-based, reactive resource provisioning in
general-purpose systems, schedulability analyses rely on statically deriving
properties that characterize the temporal worst-case behavior of the system,
and thus heavily rely on mathematical foundations.

In recent years, however, the trust in those foundations has been put to
challenge, since a considerable number of published analyses were found to be
flawed due to incorrect pen&paper proofs. Instead of attributing those issues
solely to human error, we argue that there is a fundamental problem to be
addressed in real-time scheduling theory: system models and analyses have
become increasingly complex and difficult to verify, placing a heavy burden
on authors and reviewers. Since many real-time systems target safety-critical
applications, it is crucial for such systems to be grounded on more robust
mathematical foundations.

To address this lack of trust in state-of-the-art schedulability analyses,
I will present Prosa, a long-term project for the formalization and verification
of real-time schedulability analysis, which aims to provide the theoretical
support for the next generation of certified real-time systems. To ensure full
correctness of the proofs, Prosa is written in and mechanically verified with
Coq, a powerful and mature proof assistant with support for higher-order
logic and computations.
Video Broadcast
Video Broadcast:YesTo Location:Saarbr├╝cken
To Building:E1 5To Room:422
Meeting ID:
Tags, Category, Keywords and additional notes
Attachments, File(s):
Maria-Louise Albrecht/MPI-KLSB, 09/06/2018 04:34 PM
Last modified:
Maria-Louise Albrecht/MPI-KLSB, 09/06/2018 04:38 PM
  • Maria-Louise Albrecht, 09/06/2018 04:38 PM -- Created document.