Keynotes

From Uncertain Certainty to Certain Uncertainty: 
A Reflection on a Decade of Verified Schedulability Analysis with PROSA

Björn Brandenburg, Max Planck Institute for Software Systems (MPI-SWS)

Abstract: When should designers of safety-critical real-time systems trust schedulability analysis results, despite the uncertainty caused by major errata in the literature? A decade ago, this question motivated the creation of PROSA, a library for the formalization and verification of real-time scheduling theory using the Rocq proof assistant. Since its inception in 2015, PROSA has featured in more than a dozen publications and grown into the largest continuously maintained formal library for real-time systems research. The guiding promise of PROSA then as now is simple — eliminate human error in schedulability analyses — yet its development has been anything but.  On the occasion of the project’s 10th anniversary, I take the opportunity to revisit the original motivation for PROSA, take stock of what has — and hasn’t — been accomplished, and reflect on whether such a project is still needed today. Looking forward, I will showcase how recent work based on PROSA has progressed far beyond its original scope, connecting to actual systems, software verification, stochastic models, and practical tooling. Finally, I will argue that embracing model uncertainty as a first-class analysis concern is a grand challenge for the coming decade — not only for PROSA, but for the field as a whole — and highlight  opportunities for the community to join forces in the rigorous pursuit of “certain uncertainty.”

Bio: Björn Brandenburg is a faculty member at the Max Planck Institute for Software Systems (MPI-SWS), where he leads the Real-Time Systems Group. His research focuses on the design, implementation, analysis, and verification of predictable multiprocessor real-time operating systems. His work ranges from theoretical foundations, such as multiprocessor synchronization protocols and the PROSA framework for verified schedulability analyses, to applied systems building, such as the LITMUS^RT testbed and the LiME model extractor. He has served as Program Chair of EMSOFT, RTAS, and ECRTS, and currently serves as Editor-in-Chief of Leibniz Transactions on Embedded Systems (LITES) and Program Chair of RTSS 2025. His work has been recognized with the inaugural ACM SIGBED Early Career Award (2018), an ERC Starting Grant (2019), and multiple best and outstanding paper awards.

---

Abstract: The Automotive industry is undergoing radical changes, driven by the rise of autonomous software defined vehicles, by the change of the hardware architectures, and by corresponding changes in the automotive software architectures. The talk presents a personal interpretation of the main trends happening in the automotive software world, taken from public sources, with particular attention to standardization and opensource efforts. 

Bio: Paolo Gai graduated (cum laude) in Computer Engineering at University of Pisa in 2000, and obtained the PhD from Scuola Superiore Sant’Anna in 2004.
He has been in 2002 the founder of Evidence Srl, a company providing innovations in the field of operating systems and platforms for embedded devices. Since 2019, he is working in the Huawei Pisa Research Center, focusing his work on the development of hard real-time software architectures for embedded automotive/digital power control systems. His research interests include multi and many-core processor systems, real-time operating systems, scheduling algorithms and analysis, parallel programming, and hypervisors.