April 2, 2020 | Leaf: Verification of mixed-criticality embedded systems

CEA Tech
A tool for the analysis and formal verification of the time properties of embedded computers is currently being developed at CEA List. The goal is to control cohabitation and interactions by addressing the hierarchy between functions with different criticality levels.

Increasingly complex hardware architectures and command-control algorithms are creating new challenges for the aeronautics, automotive, and other industries. Not least of which is the widening gap between average performance and worst-case scenarios. This is particularly problematic for embedded systems, where functions with different criticality levels and a variety of performance requirements must live on the same computer. The response times for embedded systems must be well-defined and controlled. However, the computing resources are dimensioned according to the worst-case response times, which are significantly overestimated to provide a safety buffer.

A more detailed assessment of the computers’ time properties (anomalies, memory contention, etc.) would enable more efficient use of the available computing resources and, in the process, make it possible to reduce the safety buffer. List turned to the University of California, Berkeley for its world-leading scientific research and targeted expertise in predictable architectures. Researchers at List subsequently started development work on Leaf, a tool that makes clever use of formal methods to very accurately reproduce, analyze, and verify program behaviors on a given computer.

Ultimately, Leaf should be able to provide information that will help manufacturers design and dimension their systems and, therefore, increase trust in system behavior.


Read article at: