Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol

We consider programs for embedded real-time systems which use priority-driven preemptive scheduling with task priorities adjusted dynamically according to the immediate ceiling priority protocol. For these programs, we provide static analyses for detecting data races between tasks running at different priorities as well as methods to guarantee transactional execution of procedures. Beyond that, we demonstrate how general techniques for value analyses can be adapted to this setting by developing a precise analysis of affine equalities. Categories and Subject Descriptors F.3.1 [Logics and meaning of programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics and meaning of programs]: Semantics of Programming Languages—Program analysis; D.2.4 [Software Engineering]: Software/Program Verification General Terms Algorithms, Theory, Verification Keywords inter-procedural analysis, abstract domains, interruptdriven concurrency

• Type: Journal
• Year: 2011
• Where: POPL
• Authors: Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich, Markus Müller-Olm
• Keywords: Abstract Domains, POPL 2011, Programming Languages, Real Time Systems, Task Priorities