Static checking of interrupt -driven software

Static checking can provide safe and tight bounds on stack usage and execution times in interrupt-driven systems. This dissertation presents static analysis algorithms and a prototype implementation of those algorithms for statically computing resource bounds in interrupt-driven systems. Advanced knowledge of resource bounds enables real-time system designers to eliminate whole classes of errors from their software before testing begins, thereby reducing the testing effort necessary to achieve confidence in their system. Despite the ubiquity of hardware interrupts in real-time systems, little prior research has dealt with interrupt-driven software. The benchmark suite of commercially-deployed, interrupt-driven systems examined here includes proprietary Z86-based microcontrollers programmed in assembly language with multiple vectored interrupt sources, a shared system stack, extensive use of unstructured loops, and no formal loop annotations. The stack analysis bounds the maximum stack size to within one byte of the true maximum in all but one of the programs in the benchmark suite. The deadline analysis found firm worst-case latencies in 30% of the cases; in the remaining 70% of the benchmarks, the prototype reduced the size of the testing problem by an average of 98%. While the testing effort still required for these systems is large, it is several orders of magnitude smaller than the testing problem without deadline analysis. This dissertation presents novel algorithms for static analysis in the context of interrupt-driven assembly code. The prototype implementation is one of the first tools to incorporate static analysis with testing oracles in an interactive fashion