Un programme annoté en vaut deux

Alain Giorgetti 1 Julien Groslambert 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : La sécurité du logiciel passe par les méthodes formelles, mais comment faire passer les méthodes formelles dans le monde réel du développement des logiciels critiques ? Cet article propose un mécanisme et un outil d'aide à la vérification de code, par réduction automatique de propriétés de sécurité en annotations formelles. Ce dispositif s'applique aux programmes Java annotés en JML. Il est illustré ici par l'annotation automatique d'une classe de l'API Java Card. Deux formalismes complémentaires pour l'expression de propriétés sont proposés. L'outil JAG, qui implante leur réduction en annotations JML, est décrit en détail. Le langage d'annotations retenu (JML) étant standard, cet outil s'interface naturellement avec de nombreux outils existants pour la vérification par preuve, test ou model-checking de Java annoté en JML.
Type de document :
Communication dans un congrès
Journée Francophone des Langages Applicatifs - JFLA07, Jan 2007, Aix-les-Bains, France. 2007
Liste complète des métadonnées

https://hal.inria.fr/inria-00181135
Contributeur : Alain Giorgetti <>
Soumis le : mardi 23 octobre 2007 - 11:35:42
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : dimanche 11 avril 2010 - 23:37:08

Fichier

GG07.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00181135, version 1

Citation

Alain Giorgetti, Julien Groslambert. Un programme annoté en vaut deux. Journée Francophone des Langages Applicatifs - JFLA07, Jan 2007, Aix-les-Bains, France. 2007. 〈inria-00181135〉

Partager

Métriques

Consultations de la notice

274

Téléchargements de fichiers

180