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
Abstract : Formal verification methods could be of much help to increase software safety. But how to transfer these methods in the real world of critical software development? This paper proposes a tooled solution for source code verification, by automated reduction of safety properties into formal assertions. This approach is applied to JML annotated Java programs. It is illustrated by the automated generation of assertions for a class from the Java Card API. Two complementary formalisms are proposed for expressing properties. Their reduction in JML annotations is implanted in the JAG tool, described with details. The output language (JML) being standard, this tool interfaces easily with many standard tools for verification of JML/Java code by proof ou model-checking.
Complete list of metadatas

https://hal.inria.fr/inria-00181135
Contributor : Alain Giorgetti <>
Submitted on : Tuesday, October 23, 2007 - 11:35:42 AM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM
Long-term archiving on : Sunday, April 11, 2010 - 11:37:08 PM

File

GG07.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨inria-00181135⟩

Share

Metrics

Record views

288

Files downloads

187