Auto-Active Verification of Software with Timers and Clocks (STAC)

Abstract

Motivation. STAC = software that accesses the system clock, exchanges clock values, and uses these values to set timers and perform computation. Key to real-time and cyber-physical systems Essential to keep software in sync with the physical world Examples = thread schedulers and time budget enforcers, distributed protocols (e.g., plug-and-play medical devices) Goal : Formally verify STACs at the source code level using deductive (aka autoactive) verification Target: ZSRM mixed-criticality scheduler- Performs thread CPU allocation and time budget enforcement- Available as Linux kernel module implemented in C- Currently we focus on ZSRM budget enforcement only.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 2016
Accession Number
AD1145653

Entities

People

  • Dionisio de Niz
  • Mark Klein
  • Sagar Chaki

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Contracts
  • Department Of Defense
  • Engineering
  • Guarantees
  • Materials
  • Software Development
  • United States
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Cybersecurity.
  • Parallel and Distributed Computing.

Technology Areas

  • Cyber