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.

PDF [5152 KB]

PRESENTATION