Auto-Active Verification of Software with Timers and Clocks

November 1, 2016 • Presentation

By

Sagar Chaki and 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.