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

Digital Library


Time-Bounded Analysis of Real-Time Systems

  • 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