Time-Bounded Analysis of Real-Time Systems
Sagar
Chaki, Arie Gurfinkel, Ofer Strichman,
Proceedings of Formal Methods in Computer-Aided Design
(FMCAD), page 72-80, October 30-November 2,
2011.
Abstract:
Real-Time Embedded Systems (RTESs) constitute an important sub-class
of concurrent safety-critical software. 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 B, we construct (and verify) a sequential program S that
over-approximates all executions of C up to time B, 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.
Online