Real-time embedded software (RTES) constitutes an important subclass of concurrent safety-critical programs. We consider the problem of verifying functional correctness of periodic RTES, a popular variant of RTES that executes 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.
This material was presented at the International
Conference on Formal Methods in Computer-Aided Design in Austin, Texas. It
introduces an approach for time-bounded verification of safety properties in
periodic RTES. We based our approach 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. The 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.