JAG : Génération d'annotations JML pour vérifier des propriétés temporelles

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
Abstract : This paper presents a tool for verifying security properties on Java code enriched with JML annotations. These temporal properties are expressed in an extension of JML. They are translated by the tool into standard JML annotations and are automatically integrated in the Java class under verification. This paper is an extended version of a paper presented at AFADL'06 tool session.
Type de document :
Rapport
[Research Report] 2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00114317
Contributeur : Alain Giorgetti <>
Soumis le : jeudi 16 novembre 2006 - 11:59:34
Dernière modification le : vendredi 6 juillet 2018 - 15:06:09
Document(s) archivé(s) le : mardi 6 avril 2010 - 19:10:33

Identifiants

  • HAL Id : inria-00114317, version 1

Citation

Alain Giorgetti, Julien Groslambert. JAG : Génération d'annotations JML pour vérifier des propriétés temporelles. [Research Report] 2006. 〈inria-00114317〉

Partager

Métriques

Consultations de la notice

260

Téléchargements de fichiers

131