|
 
|
[Ben14] Analyse de dépendances ML pour les évaluateurs de logiciels critiques
Mémoire de Thèse : Soutenue le: 16 May 2014, pp. 238, pp.: Directeur: C. Dubois, F. PessauxRapporteur 1: S. Blazy
Rapporteur 2: R. Di Cosmo
Membre du jury: David Rajchenbach-Teller
Membre du jury: M-L Potet
Membre du jury:, : Analyse de dépendances ML pour les évaluateurs de logiciels critiques,
Mots clés: analyse de dépendances, logiciels critiques, langages fonctionnels, Coq
Résumé:
Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normes en vigueur avant leur mise en service. Cette évaluation est obtenue après un long travail d’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidés par des outils utilisés de manière interactive pour construire des modèles, en faisant appel à des analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulière sur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Ce travail présente une analyse de flot d’information pour de tels langages, spécialement conçue pour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’une interprétation abstraite de la sémantique opérationnelle préalablement enrichie par des informations de dépendances. Elle est prouvée correcte vis-à -vis d’une définition formelle de la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue une base théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes.
Equipe:
sys
BibTeX
| @phdthesis { | |||
| Ben14, | |||
| title | = | "{ Analyse de dépendances ML pour les évaluateurs de logiciels critiques}", | |
| author | = | "V. Benayoun", | |
| year | = | 2014, | |
| pages | = | "238", | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| note | = | "{ Directeur: C. Dubois, F. Pessaux Rapporteur 1: S. Blazy Rapporteur 2: R. Di Cosmo Membre du jury: David Rajchenbach-Teller Membre du jury: M-L Potet Membre du jury:}", | |
| } |
