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

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

Presentation

Time-Bounded Analysis of Real-Time Systems

  • October 2011
  • By Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman
  • This presentation considers the problem of verifying functional correctness of periodic Real-Time Embedded Software (RTES), a popular variant of RTES that execute periodic tasks in an order determined by Rate Monotonic Scheduling (RMS).
  • Cyber-Physical Systems
  • Publisher: Software Engineering Institute
  • Abstract

    Real-Time Embedded Software (RTES) constitutes an important sub-class of concurrent safety-critical programs. We consider the problem of verifying functional correctness of periodic RTES, a popular
    variant of RTES that execute periodic tasks in an order determined by Rate Monotonic Scheduling (RMS). A computational model of a periodic RTES is a finite collection of terminating tasks that arrive
    periodically and must complete before their next arrival. We present an approach for time-bounded verification of safety properties in periodic RTES. Our approach is based on sequentialization. Given an RTES C and a time-bound W, we construct (and verify) a sequential program S that over-approximates all executions of C up to time W, while respecting priorities and bounds on the number of preemptions
    implied by RMS.Our algorithm supports partial-order reduction, preemption locks, and priority locks. We implemented our approach for C programs, with properties specified via user-provided assertions. We evaluated our tool on several realistic examples, and were able to detect a subtle concurrency issue in a robot controller.

  • Download