Analysis of real-time code by model checking

The technical contribution of this paper is a particular way of adding model-checking to the repertoire of more familiar techniques (such as rate monotonic analysis) for analyzing real-time behavior. Model-checking comprises automated methods of search and reasoning that apply, in principle, to any system representable as a finite state machine. It can be used to verify not only that deadlines are met but other system properties as well. The methods we propose are general, but are applied in the context of a specific solution to the problem of safety-critical runtime support. The Ravenscar subset of Ada tasking is designed to support pre-emptive scheduling while requiring minimal runtime support. The Ravenscar profile is supported by the RAVEN^TM runtime, developed at Aonix to be FAA certifiable. Our immediate goal is to verify Ravenscar programs running on RAVEN^TM