Sagar Chaki

Sagar Chaki, Arie Gurfinkel, Ofer Strichman, Proceedings of Formal Methods in Computer-Aided Design (FMCAD), page 72-80, October 30-November 2, 2011.

Software: Tools and benchmarks for experiments reported in the paper are here. Read LICENSE.txt for the license, and README.txt for usage.

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.