Master’s Thesis: The Time is Right: Retrofitting Formal Verification onto Timers in an Operating System
Published:
Operating systems need timers to function correctly. Despite their critical nature, timers are notoriously difficult to test for correctness. This thesis formally verifies the correctness of a timer virtualization layer in an embedded operating system. We prove that all timers are scheduled correctly, and every callback fires according to the OS specification. We introduce a framework to model timers and present an experience report on the state of retrofitted formal verification.
Thesis Statement: The path to a world of verified software is through the gradual instrumentation of formal verification onto existing systems. Retrofitting invariants onto legacy codebases, rather than rewriting from scratch, is both practical and necessary. This thesis demonstrates that incremental introduction of formal guarantees into real-world systems is feasible, lowering adoption barriers and enabling broader formal methods impact in software engineering. This thesis contributes a methodology to retrofit verification onto existing systems code, bringing us closer to a future of understandable and safe software. We remove one barrier to widespread formal verification adoption.
The thesis is licensed CC BY-NC-SA 4.0 (Attribution-NonCommercial-ShareAlike 4.0 International).
