search menu icon-carat-right cmu-wordmark
Carnegie Mellon University

Software Engineering Institute

  1. SEI
  2. Publications
  3. Digital Library
  4. Auto-Active Verification of Software with Timers and Clocks

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

Watch

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.