Verification of class liveness properties with Java modeling languageReport as inadecuate




Verification of class liveness properties with Java modeling language - Download this document for free, or read online. Document in PDF available to download.

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, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications 2 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies

Abstract : Static checking is key for the security of software components. As a component model, this paper considers a Java class enriched with annotations from the Java Modeling Language JML. It defines a formal execution semantics for repetitive method invocations from this annotated class, called the class in isolation semantics. Afterwards, a pattern of liveness properties is defined, together with its formal semantics, providing a foundation for both static and runtime checking. This pattern is then inscribed in a complete language of temporal properties, called JTPL Java Temporal Pattern Language, extending JML. We particularly address the verification of liveness properties by auto- matically translating the temporal properties into JML annotations for this class. This automatic translation is implemented in a tool called JAG JML Annotation Generator. Correctness of the generated annotations ensures that the temporal property is established for the executions of the class in isolation.

Mots-clés : liveness temporal logic Java language JML assertion





Author: Alain Giorgetti - Julien Groslambert - Jacques Julliand - Olga Kouchnarenko -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents