Static Analysis of Interrupt-Driven Programs

  • Prof. Dr. Helmut Seidl | Technical University of Munich

OSEK/AUTOSAR is an industrial standard of the European automotive industry for hard realtime tasks. This talk explains the underlying scheduling policy and presents static analyses of subtle concurrency properties such as potential dataraces or transactionality. Also, we explain how these analyses allow to identify and verify hand-crafted synchronization patterns that circumvent the primitives offered by OSEK.