AYRAULT Philippe
رئاسـة البـحث : Thérèse HARDIN
تأطـير مـشـترك : PESSAUX François
Développement de logiciels critiques en Focalize. Méthodologie et outils pour l'évaluation de conformité
Cette thèse repose sur l’expérience de l’auteur, en tant qu’évaluateur de systèmes critiques pilotés par du logiciel et porte sur les besoins en support théorique et en formalisation des études de risque, afin de conforter les décisions de mise en exploitation. Après un état de l’art sur la sûreté, la thèse porte sur deux aspects de la certification d’un logiciel critique développé avec l’atelier de développement Focalize. Celui-ci permet l’écriture de spécifications sous la forme de formules du premier ordre puis le développement progressif du code, en utilisant héritage, paramétrisation et modularité. Tout d’abord, un cycle de développement système couvrant l’ensemble des phases de la spécification à la maintenance est proposé pour Focalize et sa conformité aux exigences requises par les normes de la Sûreté est montrée. La thèse porte ensuite sur la réalisation d’analyses de risques sur un logiciel développé en Focalize. Un outil de calcul de dépendances entre Entrées/Sorties vraies d’un composant est spécifié formellement en Coq et sa preuve de correction est fournie.
مناقـشـة مـذكـرة : 22/04/2011
أعـضاء لجنة المناقـشة :
Marie-Laure Potet (Pr. ENSIMAG-VERIMAG) [rapporteur]
C. Kirchner [rapporteur]
T. Hardin
F. Pessaux
V. Viguié Donzeau-Gouge
C. Queinnec
P.E. Moreau
Richard Imhoff (Conseiller Technique et Assurance Sécurité, THALES Rail Signaling)
إصدارات 2000-2012
-
2012
- F. Pessaux, V. Benayoun, C. Dubois, Ph. Ayrault : “ML Dependency Analysis for Assessors”, Software Engineering and Formal Methods (SEFM) 2012, vol. 7504, Thessaloniki, Greece, pp. 278-292, (Springer Verlag) (2012)
-
2011
- Ph. Ayrault : “Développement de logiciels critiques en Focalize. Méthodologie et outils pour l’évaluation de conformité”, أطروحة, مناقـشـة مـذكـرة 22/04/2011, رئاسـة البـحث Hardin, Thérèse, تأطـير مـشـترك : Pessaux, François (2011)
-
2009
- Ph. Ayrault, Th. Hardin, F. Pessaux : “Development of a Generic Voter under FoCal”, Proceedings of the 3rd International Conference on Tests and Proofs, vol. 5668, Lecture Notes in Computer Science, Zurich, Switzerland, pp. 10-26, (Springer) (2009)
- Ph. Ayrault, Th. Hardin, F. Pessaux : “Development life cycle of critical software under FoCal”, Electronic Notes in Theoretical Computer Science, vol. 243, pp. 15-31, (Elsevier) (2009)
-
2008
- Ph. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez, L. Habib, Th. Hardin, M. Jaume, Ch. Morisset, F. Pessaux, R. Rioboo, P. Weis : “Trusted Software within Focal”, Trusting Trusted Computing ?, Rennes, France, pp. 162-179 (2008)
-
2000
- Ph. Ayrault, M. Guesdon, Th. Hardin : “Méthodologie de développement d’un outil d’évaluation de la sureté du logiciel, en langage OCaml”, Journées Francophones des Langages Applicatifs, INRIA, Mont Saint-Michel, France, pp. 159-171 (2000)