News 2017

Cyber-Physical Systems

Two MPI-SWS faculty awarded DFG grants

December 2017
Two MPI-SWS faculty members have received 3-year research grants from DFG, the German Research Organization.

Eva Darulova has received a single-PI DFG grant entitled "Automated Rigorous Verification and Synthesis of Approximations." Björn Brandenburg has received a DFG grant entitled "RT-Proofs: Formal proofs for real-time systems." This award is for a collaborative grant, with co-PIs at INRIA (Grenoble), Verimag (Grenoble), ONERA (Toulouse), and TU Braunschweig (Germany).

Both projects are actively recruiting doctoral students. Interested students can apply online.

Automated Rigorous Verification and Synthesis of Approximations

Computing resources are fundamentally limited and sometimes an exact solution may not even exist. Thus, when implementing real-world systems, approximations are inevitable, as are the errors introduced by them. The magnitude of errors is problem-dependent but higher accuracy generally comes at a cost in terms of memory, energy or runtime, effectively creating an accuracy-efficiency tradeoff. To take advantage of this tradeoff, we need to ensure that the computed results are sufficiently accurate, otherwise we risk disastrously incorrect results or system failures. Unfortunately, the current way of programming with approximations is mostly manual, and consequently costly, error prone and often produces suboptimal results.

The goal of this project is to develop an end-to-end system which approximates numerical programs in an automated and trustworthy fashion. The programmer will be able to write exact high-level code and our `approximating compiler' will generate an efficient implementation satisfying a given accuracy specification. In order to achieve this vision, we will develop novel sound techniques for verifying the accuracy of approximate numerical programs, as well as new synthesis approaches to generate such approximations automatically.

RT-Proofs: Formal proofs for real-time systems

Real-time systems, i.e., computer systems subject to stringent timing constraints, are at the heart of most modern safety-critical technologies, including automotive systems, avionics, robotics, and factory automation, to name just a few prominent domains in which incorrect timing can have potentially catastrophic consequences. To assure the always-correct operation of such systems, i.e., to make sure that they always react in a timely fashion even in a worst-case scenario, rigorous validation efforts are required prior to deployment. However, establishing that all timing constraints are met is far from trivial --- and requires sophisticated analysis techniques --- because software timing varies in complex and difficult to predict ways, e.g., due to scheduling delays, shared resources, or communication, even when executing on a dedicated processor. Unfortunately, the theoretical foundations of current analysis methods are not nearly as rock-solid as one might expect.

The key problem is that the state-of-the-art methods are backed by only informal or abbreviated proofs, which are typically difficult to understand, check, adapt, or reuse. As a result, there is a non-trivial risk of subtle, but fatal mistakes, either lingering in the published literature, or arising when combining results with unstated, inconsistent assumptions. And indeed, this is not just a hypothetical concern --- most famously, the timing analysis of the CAN real-time bus (widely deployed in virtually all modern cars) was refuted in 2007, 13 years after initial publication. Similarly, other lesser-known examples of incorrect worst-case analyses abound in the literature, including off-by-one errors, incorrect generalizations, and even claims that are simply wrong. Worse, even if the underlying theory is indeed flawless, there is still no guarantee that it is actually implemented correctly in the toolchains used in practice. In short, the state of the art in the analysis of safety-critical real-time systems leaves a lot to be desired --- informal "pen and paper" proofs are simply inadequate.

There is a better way: timing analysis results should be formally proved, machine-checkable, and independently verifiable. To this end, the RT-proofs project will lay the foundations for the computer-assisted verification of schedulability analysis results by (i) formalizing foundational real-time concepts using the Coq proof assistant and (ii) mechanizing proofs of busy-window-based end-to-end latency analysis, the analysis approach of greatest practical relevance (e.g., used by SymTA/S). Additionally, we will (iii) demonstrate with a practical prototype how trust in a vendor's toolchain can be established by certifying the produced analysis results (rather than the tool itself). Leading by example, RT-proofs will fundamentally raise the level of rigor, to the benefit of the academic community, tool vendors, and real-time systems engineers in practice.

MPI-SWS researchers win RTAS 2017 Best Paper award

December 2017
Pratyush Patel, Manohar Vanga, and Björn Brandenburg have won the Best Paper award at the 23rd IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2017) for their paper entitled "TimerShield: Protecting High-Priority Tasks from Low-Priority Timer Interference".

MPI-SWS paper accepted into RTSS'17

July 2017
The paper entitled "An Exact and Sustainable Analysis of Non-Preemptive Scheduling" by MPI-SWS researchers Mitra Nasri and Björn Brandenburg was accepted into the program of the 38th IEEE Real-Time Systems Symposium (RTSS 2017).

RTSS 2017 will be held from December 6 to December 8 in Paris, France.


MPI-SWS researchers win RTAS 2017 Outstanding Paper award

April 2017
Mitra Nasri and Björn Brandenburg have won an Outstanding Paper award at the 23rd IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2017) for their paper entitled "Offline Equivalence: A Non-Preemptive Scheduling Technique for Resource-Constrained Embedded Real-Time Systems".

Principles of Cyber-Physical Systems Course at TU Kaiserslautern

April 2017
Sadegh Soudjani is teaching Principles of Cyber-physical Systems at the University of Kaiserslautern in Summer 2017.

The course meets Tuesdays 11:45-13:15 and Thursdays 10:00-11:30 in 11-260.

Advanced Automata Theory Course at TU Kaiserslautern

April 2017
Rupak Majumdar and Daniel Neider are co-teaching Advanced Automata Theory at the University of Kaiserslautern in the Summer 2017 semester.

The course meets Tuesdays 08:15-09:45 in room 48-210 and Wednesdays 13:45-15:15 in room 46-280 on the University of Kaiserslautern campus.