ML Dependency Analysis for Assessors

Autor: Vincent Benayoun, François Pessaux, Philippe Ayrault, Catherine Dubois
Přispěvatelé: Sûreté et Fiabilité des Logiciels (SFL), Unité d'Informatique et d'Ingénierie des Systèmes (U2IS), École Nationale Supérieure de Techniques Avancées (ENSTA Paris)-École Nationale Supérieure de Techniques Avancées (ENSTA Paris), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Sémantiques, preuves et implantation (SPI), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)
Jazyk: angličtina
Rok vydání: 2012
Předmět:
Zdroj: Software Engineering and Formal Methods (SEFM) 2012
Software Engineering and Formal Methods (SEFM) 2012, Oct 2012, Thessaloniki, Greece. pp.278-292, ⟨10.1007/978-3-642-33826-7_19⟩
Software Engineering and Formal Methods ISBN: 9783642338250
SEFM
DOI: 10.1007/978-3-642-33826-7_19⟩
Popis: International audience; Critical software needs to obtain an assessment before com- missioning. This assessment is given after a long task of software analysis performed by assessors. They may be helped by tools, used interactively, to build models using information-flow analysis. Tools like SPARK-Ada exist for Ada subsets used for critical software. But some emergent lan- guages such as those of the ML family lack such adapted tools. Pro- viding similar tools for ML languages requires special attention on spe- cific features such as higher-order functions and pattern-matching. This paper presents an information-flow analysis for such a language specifi- cally designed according to the needs of assessors. This analysis can be parametrized to allow assessors getting a view of dependencies at several levels of abstraction and gives the basis for an efficient fault tolerance analysis.
Databáze: OpenAIRE
Externí odkaz: