Affiliation

Marco Panunzio
Department of Pure and Applied Mathematics, University of Padua
via Trieste 63
35121 Padova
Italy

Temporal Isolation with the Ravenscar Profile and Ada 2005

Enrico Mezzetti, Marco Panunzio and Tullio Vardanega

14th International Real-Time Ada Workshop

Abstract

Modern methodologies for the development of high-integrity real-time systems build on abstract representations or models instead of code artifacts. Since analysis techniques are applied to models, it is important that system properties asserted during the analysis and the assumptions made for the analysis to hold are preserved across implementation and execution. In this paper we highlight that the extent of properties preservation we require cannot be warranted using exclusively the language constructs allowed by the Ravenscar Profile. Hence, in the light of the new Ada 2005 features, we propose the formalization of a new augmented profile, fit for the purpose and yet still adhering to the Ravenscar rationale.