Auto-Active Verification of Software with Timers and Clocks
November 2016 • Presentation
Sagar Chaki, Dionisio de Niz
Software that accesses the system clock is the key to real-time and cyber-physical systems
Software Engineering Institute
The goal of this work is to formally verify software with timers and clocks (STACs) at the source code level using deductive (also known as auto-active) verification. Our target is the ZRSM mixed-criticality scheduler.