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.
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.
This wastes time because the machine could perform some operations simultaneously. To implement simultaneous movements, Kong programmed multiple tasks along with their constraints. For example, the head can move toward the tape while the tape advances to the next position, but then the tape must hold still so the color sensor can read it. The writer lever and the head can move simultaneously, but they must avoid physical collision. This multitasking with constraints provided an application for the START program to test the verification tool to ensure that an implementation has all the desired concurrency properties.
For more information
Please tell us what you
think with this short
(< 5 minute) survey.