Static Analysis of Interrupt-driven Programs Synchronized via the Priority Ceiling Protocol

uni-muenster.de 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 meth-ods 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 mean-ing of programs]: Specifying and Verifying and Reasoning abou