The Static Analysis of Real-Time Systems (START) project is part of the SEI's research in cyber-physical systems. The goal of this project is to verify the concurrency properties of real-time embedded software (RTES). The current focus is on time-bounded analysis of RTES. We aim to verify whether an assertion X can fail when the RTES is executed for B units of time from an initial state I. We assume that the RTES is written in C and consists of a set of periodic tasks with rate monotonic scheduling. We also assume that the RTES is schedulable and that the user knows the priority and worst-case execution time of each task. The user specifies the time-bound B, assertion X, and initial state I.

We are releasing three prototype tools that implement our solution along with instructions for their use. To download these tools, as well as experimental results and a technical report, visit the START project web page hosted at Carnegie Mellon University.