The OSEK operating system is a 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 analyzes exist for single and multi-The OSEK operating system is a automotive standard relying on priority scheduling and interrupts. The work presented here provides methods to leverage the vast ecosystem of abstract interpretation to programs with preemptive scheduling and interrupts. The key contributions are analyses of priorities, resources and flags. Based on these analysis techniques are presented that allow the precise detection of data-races in OSEK programs.     «

The OSEK operating system is a 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 analyzes exist for single and multi-The OSEK operating system is a automotive standard relying on priority scheduling and interrupts. The work presented here provides methods to leverage the vast ecosystem of abstract interpretation to programs wi...     »