Multi-Criticality Real-time Systems

Multi-Criticality Real-time Systems is a research activity of the Trustworthy Systems project inside the Software System Research Group (SSRG).

• Aim: develop a trustworthy platform for building multi-criticality real-time systems.

• Overview: Many trusted systems (i.e. systems whose safety, security or reliability we trust) must deliver a response to an external stimulus within a certain time period, and are therefore critical real-time systems. These include medical implants (e.g. pacemakers), avionic systems and industrial controllers. A failure to perform a computation or operation within a given time may have catastrophic consequences in these environments.

  Such systems are increasingly complex. An example are wearable or implanted medical devices, which combine life-supporting functionality with user interfaces to allow monitoring by the patient or network drivers and protocol stacks for remote monitoring. Other devices contain multiple real-time functions with different levels of criticality, such as automotive safety and control systems.

  Subsystems of different criticality must be strongly isolated, in order to prevent malfunction of a less critical function affecting a highly-critical one. This isolation is often achieved by physical separation, however, this is frequently impossible, due to space and energy constraints (e.g. in medical implants) or where the number of different functions is becoming too large (e.g. in cars).

  Trustworthiness of such a system can only be achieved if strong functional as well as temporal isolation (with tightly-controlled communication) can be guaranteed between subsystems. This puts stringent requirements on the underlying operating system, whose job it is to provide this isolation. Our real-time systems work aims at providing this foundation for trustworthiness. We focus primarily on the seL4 microkernel, as its formal verification already eliminates many sources of failure. Additional requirements for supporting multi-criticality systems include:

  • specification and analysis to the temporal properties of seL4-based systems
  • appropriate kernel mechanisms for supporting scheduling and isolated execution of multiple real-time and best-effort programs on seL4.

• Temporal properties of seL4-based systems: A prerequisite for reasoning about temporal properties of software running in protected mode is an understanding of the worst-case execution time (WCET) of kernel operations, in particular, interrupt latencies. Here we are working on:

  • Computing the worst-case execution time (and thus interrupt latency) of seL4. We have succeeded in a complete, sound analysis of latencies of all kernel operations on modern ARM processors (ARM11 and Cortex A8). This is the first ever published complete timing analysis of a protected multitasking kernel.
  • Improving the worst-case execution time of seL4, whilst maintaining its verifiability. This involves careful examination and adaptation of the kernel design and implementation.
  • Improving the average-case performance of seL4, again while maintaining verifiability. This improves schedulability of lower-criticality workloads.

• Kernel mechanisms for real-time systems: We are evolving the seL4 API to support general multi-criticality systems. This involves investigating the most appropriate kernel mechanisms for scheduling real-time tasks and ensuring their temporal isolation. We are also investigating how seL4's capability-based resource-management model can be extended to cover time as a resource.

  Presently we are working on understanding the requirements for such kernel mechanisms, by mapping various real-time systems onto seL4. This includes work on porting the Fiji JVM from Fiji Systems to seL4.

• Previous research: NICTA's Potoroo project investigated the real-time properties of L4 kernels. Our current work builds upon this, but with fresh ideas, new approaches and the verified foundation of seL4.

People