Sciweavers

Share
POPL
2011
ACM

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

7 years 9 months ago
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
Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Pe
Added 17 Sep 2011
Updated 17 Sep 2011
Type Journal
Year 2011
Where POPL
Authors Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Peter Lammich, Markus Müller-Olm
Comments (0)
books