The goal of the Static Analysis of Real-Time Systems (START) project is to verify functional correctness of real-time embedded software (RTES). The current focus is on model checking periodic RTES with Rate-Monotonic scheduling, a.k.a, periodic programs. Such programs are widely used in the automotive and avionics domains. Specifically, we verify whether an assertion Spec can fail when the RTES is executed from an initial state Init. 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 assertion Spec, and initial state Init. In past work, we also required a user-supplied time bound Bound that limits the execution of the software. In ongoing work, we are eliminating this requirement (i.e., we will verify correctness of a periodic program even if it executes for unbounded time).
Papers, tools, examples, and experimental results are available here.
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 right a 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 sequential-operation performance 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.