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.
We are releasing a prototype tool, called REK, that implements our solution, and benchmarks and results we have used for empirical evaluation of REK. Once you download and unpack the distribution, read the README for further instructions. REK should run on a modern Linux distribution (we have used them on Ubuntu 9.04, 10.04 and 11.04). Full details of our experimental results are here. A paper describing this version of the tool is available here.
We are releasing a prototype tool, called REK-H, that implements our solution, and benchmarks and results we have used for empirical evaluation of REK-H. Once you download and unpack the distribution, read the README for further instructions. REK-H runs on a modern Linux distribution (we have used them on Ubuntu [9-12].04).
We are releasing a prototype tool, called REK-PIP, that extends REK-H with support for priority inheritance locks and deadlock detection. Download and unpack the distribution, read the README for further instructions. REK-PIP runs on a modern Linux distribution (we have used it on Ubuntu [9-12].04).