Static analysis of embedded software with priority scheduling and interrupts

The OSEK operating system is a widely used automotive standard relying on priority scheduling and interrupts. The peculiarities of embedded systems, especially the presence of interrupts, make static analysis of such systems a challenging task. While a lot of good analyses exist for single and multi-threaded programs, the results for concurrent embedded systems were not satisfactory, mainly due to the different scheduling paradigms. The work presented here provides methods to leverage the vast ecosystem of abstract interpretation to programs with preemptive scheduling and interrupts. One difficulty of interrupt-driven programs is that interrupts introduce a form of concurrency, thus resulting in unexpected program behavior. As one benchmark problem, a notion of data-races for OSEK programs is considered and it is shown how to exploit the intricate properties of the priority scheduling, and especially the priority ceiling protocol to construct a precise analysis. Surprisingly, real world OSEK programs often do not rely on the protection mechanisms provided by the operating system but introduce hand-crafted synchronization primitives. For a large class of such programming patterns based on flag variables, a dedicated analysis is provided that allows the verification of race freedom as well as to expose subtle bugs in these ad-hoc protocols.