search menu icon-carat-right cmu-wordmark

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

Publisher:

Software Engineering Institute

Abstract

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.