MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

PROSA: A Foundation for Verified Schedulability Analysis

Felipe Augusto Queiroz de Cerqueira
MMCI
SWS Student Defense Talks - Thesis Proposal
SWS  
Public Audience
English

Date, Time and Location

Monday, 10 September 2018
16:00
60 Minutes
G26
111
Kaiserslautern

Abstract

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.

Contact

--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
422
passcode not visible
logged in users only

Maria-Louise Albrecht, 09/06/2018 16:38 -- Created document.