The TOROS Project

A Theory-Oriented Real-Time Operating System
for Temporally Sound Cyber-Physical Systems

“Move the RTOS closer to analysis, the analysis closer to reality, and ensure that the analysis can be trusted.”

Note: Several fully funded PhD and Postdoc positions open — see details below!

Overview

The TOROS project, kindly supported by an ERC Starting Grant (2019–2024), targets the challenge of implementing safety-critical cyber-physical systems (CPSs) on commodity multicore processors such that their temporal correctness can be certified in a formal, trustworthy manner.

Motivation

While today it is in principle possible to construct a CPS in a temporally sound way, in practice this rarely happens for any but the most critical applications because, with the current real-time foundations, the prerequisite investments in time, expertise, and resources are prohibitive — simply put, it is still too complicated and too expensive, and the barrier to entry thus remains high.

Specifically, the TOROS project is motivated by three fundamental shortcomings in the design of state-of-the-art real-time operating systems (RTOSs) and the applicable timing analyses:

As a result, the use of ad-hoc, unsound “guesstimated safety margins” prevails in practice.

Goals

The TOROS project seeks to make temporally sound CPS design and implementation an economically viable choice — for most CPS applications, most of the time — by moving the RTOS closer to analysis, the analysis closer to reality, and by ensuring that the analysis can be trusted. Specifically, the TOROS project aims to

  1. introduce a radically new, theory-oriented RTOS that by design ensures that the temporal behavior of any workload can be analyzed (even if the application developer is unaware of the relevant theory),
  2. develop a matching novel timing analysis that allows for below-worst-case provisioning with analytically sound safety margins that yields meaningful probabilistic response-time guarantees, and
  3. mechanize and verify all supporting scheduling theory with the Coq proof assistant using the Prosa framework.

Ultimately, the goal is to make temporal soundness easy and affordable — the TOROS vision is to entice to analyze.

Position Paper

The motivation driving the TOROS project and a high-level sketch of the envisioned solution is provided in the following position paper.

Curious? Critical? Unconvinced? You have a great idea we should know about? Get in touch!

Open Positions

The TOROS project welcomes applications for several fully funded, 100% research, 0% nonsense positions at the level of doctoral students or postdoctoral researchers at the Max Planck Institute for Software Systems (MPI-SWS).


  1. Research assistant (PhD position in the MPI-SWS graduate program)
  2. Research assistant (PhD position in the MPI-SWS graduate program)
  3. Research assistant (PhD position in the MPI-SWS graduate program)
  4. Postdoc position (1–3 years)
  5. Postdoc position (1–3 years)
  6. Postdoc position (1–3 years)

In case of any questions, please get in touch. The TOROS project seeks to fill one or more of these roles at the earliest possible time, and also welcomes unsolicited applications for roles not explicitly listed above.

To apply, please submit an application using the MPI-SWS application portal (you need to create an account), mention the TOROS project in your application, and email the PI (Björn Brandenburg).

Team


And maybe you… come join us!

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 803111).