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.