Generation of Certified Code for Object Oriented Applications specification, refinement, proof and error detection

This project aims at developing methods and tools for the design of object-oriented systems that require a high degree of security. The methods and tools will be developed such that together they will form a coherent design method from specification to certified code generation using refinement, simulation, testing and verification techniques. In particular, the project focuses on the design of smart card applications, written in a subset of Java (like JavaCard), annotated with JML specifications. JML, the Java Modeling Language, is a source code level behavioural specification language for Java that is designed to be easy to understand for people with Java knowledge. Several tools exist which manipulate JML annotated programs, e.g. to generate documentation or tests (either dynamic or unitary) or to do automatic or interactive verification. The readability of JML specifications and the wide range of tools available for JML make it attractive for industry to integrate formal methods (in the form of JML specifications) in their software development process.

Research activities
  Verification
  Program proof
  

Participants


More information : http://geccoo.lri.fr/