Ada Ravenscar Profile and C language: Rules Porting and Compatibility Checks Automation

The Ada Ravenscar profile is a subset of the Ada language which restricts Ada tasking features in order to provide the determinism required by hard real-time systems. Some of the Ravenscar rules are based on specific Ada constructs, which are not available in other languages, but the reasoning behind each rule can be applied also to different ones. The main objective of this paper is to show how the Ravenscar profile can be adapted to work in a system where the tasking features are managed by RTEMS, and C/Ada languages work together. Furthermore, a tool developed to automate Ravenscar compliance checks is presented and applied in the context of some experimental verification activities.