Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Presentation

Auto-Active Verification of Software with Timers and Clocks

  • November 2016
  • By 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.

  • Download

Part of a Collection

SEI 2016 Research Review