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.
The LEGO Turing Machine
A Turing machine is the simplest form of computer. It is composed of a ribbon of paper called a tape, which stores data on a head that can read symbols on the tape, write a new symbol, and move left or righta list of transitions that tells the machine what to do next. Soonho Kong, a PhD student at Carnegie Mellon University, interned at the SEI in the summer of 2012 and built a LEGO Turing machine to demonstrate the START verification tool. Kong began by implementing a single task, and then added more features incrementally to create a multitasking machine.First, Kong programmed the LEGO Turing machine to perform Read, Write, and Move operations one at a time. You can see it in action in the following video.