Profil Ravenscar
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche à compléter concernant l'informatique, vous pouvez partager vos connaissances en le modifiant. |
Le profil Ravenscar est un sous ensemble du langage Ada dédié aux systèmes temps réel nécessitant une grande sûreté de fonctionnement.
L'idée est de permettre de prouver formellement les programmes écrits selon ce profil. Le profil Ravenscar en interdisant un certain nombre de caractéristiques du langage Ada, permet de rendre applicables les outils de preuve de programme.
Ce profil a aussi été appliqué à la spécification temps réel RTSJ du langage Java[1].
[modifier] References
- Alan Burns « The Ravenscar Profile » dans ACM SIGAda Ada Letters Décembre 1999, vol XIX issue= 4 pages= 49-52 [lire en ligne]
- Alan Burns, Brian Dobbing and Tullio Vardanega « Guide for the use of the Ada Ravenscar Profile in high integrity systems » dans ACM SIGAda Ada Letters, Juin 2004, vol.XXIV issue= 2 pages= 1-74 [lire en ligne]
- AI95-00249 — Ravenscar profile for high-integrity systems
[modifier] Notes
- ↑ J. Kwon, A. Wellings, and S. King, « Ravenscar-Java: A High Integrity Profile for Real-Time Java», York Technical Report (YCS 342), Department of Computer Science, University of York, 2002, [lire en ligne]
