START: Static Analysis of Real-Time Systems

The goal of this project is verification of concurrency properties of Real-Time Embedded Software (RTES). The current focus is on time-bounded analysis of RTES, i.e., verifying 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 the priority and Worst Case Execution Time (WCET) of each task is known. The time bound B, assertion X, and initial state I are specified by the user. The project is part of the research in Cyber-Physical Systems at the Software Engineering Institute.