Qui sommes-nous ?
Espace utilisateur
Formation continue
Credit : L. Godart/CEA
D’un jour à plusieurs semaines, nos formations permettent une montée en compétence dans votre emploi ou accompagnent vers le retour à l’emploi. 
Conseil et accompagnement
Crédit : vgajic
Fort de plus de 60 ans d’expériences, l’INSTN accompagne les entreprises et organismes à différents stades de leurs projets de développement du capital humain.
Thèses
Accueil   /   Post Doctorat   /   Contrats publics et privés pour ACSL

Contrats publics et privés pour ACSL

Cybersécurité : hardware et software Défis technologiques Informatique et logiciels Sciences pour l’ingénieur

Résumé du sujet

Frama-C est une plateforme collaborative de l'analyse de programmes écrits en C. Cette plateforme comprend un langage de spécification nommé ACSL basé sur la notion de contrat. Ces contrats, fournis via des annotations dans le code, permettent de spécifier ce que l'on attend des différentes fonctions d'un programme. Il est ensuite possible de vérifier que le programme est conforme aux différents contrats à l'aide des analyseurs de la plateforme.
Une limitation actuelle des contrats vis-à-vis du langage C est qu'ils ne permettent pas facilement de spécifier des contrats différents (interne/privé, externe/public) pour des modules d'un système lorsque ceux-ci cachent les détails d'implémentation aux modules utilisateurs. Pour cela, une différenciation entre contrat public et contrat privé est nécessaire, mais également les moyens de faire le lien entre les deux pour assurer la cohérence globale de la spécification et de l'analyse.

Laboratoire

Département Ingénierie Logiciels et Systèmes (LIST)
LSL (DILS)
Laboratoire pour la Sûreté du Logiciel
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down