Motivation
We are increasingly relying on small embedded computer systems and in many cases we don't even realise that we do that. Think, of example, of your mobile phone, your car, or your washing machine.
For many of these embedded computer systems, it is not only important to produce the right result, but also to produce that result within a given time frame. A good example is the airbag system of a more upmarket car. From various inputs distributed around the car the embedded system computes which of the airbags it should activate. For obvious reasons this computation needs to be performed in limited time, defined by physical characteristics, like the expected speed of the vehicle, the distance between body and airbag as well as the time required to fully inflate the airbag and others. At the same time embedded systems become increasingly complex and thus require the use of an operating system to manage that complexity. When this observation is combined with the above it becomes clear that an analysis of the temporal behaviour of the operating system is required.
Project Aim
Traditional methods of analysing the temporal behaviour of critical software by hand or measuring end-to-end and adding safety margins are subject to either a complexity barrier or deliver unreliable results respectively. Pure static analysis approaches have at the very least issues when it comes to portability. Within this project codenamed Potoroo we address real world requirements by providing an on-the-spot analysis of the operating system kernel by taking measurements on a fine granular level and using static analysis techniques to ensure that the worst case has been observed. This complements the work of the L4.verified project which aims to mathematically proof functional correctness of the seL4 microkernel.
The project is scheduled to be completed in 2008.
Who will benefit
The research is targeted as dual purpose analysis. In the hands of a real-time expert, it can be used to provide bounds on the worst-case behaviour of the kernel primitives and subsequently these may be used to calculate bounds of the worst-case response times of the system, like in the above airbag example. Similarly best-case scenarios may be explored. This in turn is required for analysis of distributed systems. When operated by a kernel programmer it may be used for hot spot identification as well as performance optimisation.
Limitations and Assumptions
The base approach using measurements carries a small risk of being an underestimation in case of insufficient measurement coverage. The approach we are following to alleviate this is by employing static analysis methods on a partial model of the processor and comparing the results of that with measurements. Limiting ourselves to modelling only the part of the processor which is responsible for the large part of variation in the execution time is driven by the fact that modelling a modern, high-performance processor in all detail is next to impossible due to the lack of documentation.
While the project aims to automate the analysis process to a large degree, expert knowledge will still be required to analyse a given system. This was a deliberate decision to ensure high portability of the analysis, which is essential when the analysis is applied to an evolving, dynamic code base deployed on various hardware platforms.
More technical detail can be found in the technical overview.