High Integrity Ravenscar

The Ravenscar Profile is now established as providing the basic building blocks for constructing high integrity Ada95 concurrent programs. The profile has been accepted for inclusion in the next revision of the Ada language standard and is already supported by the major Ada product vendors. The paper identifies the kinds of static analysis that can be performed on a concurrent Ada program that conforms to the Ravenscar profile. Furthermore, it shows how these forms of analysis can be made sufficient to eliminate all of the various forms of erroneous behaviour, bounded error conditions and implementation defined behaviour defined by the profile. Finally, a practical implementation, based on extensions to SPARK, is described.