{JML}-based Verification of Liveness Properties on a Class in isolation

Julien Groslambert (1) , Jacques Julliand (1) , Olga Kouchnarenko (1, 2)

1 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
2 CASSIS - Combination of approaches to the security of infinite states systems

This paper proposes a way to verify temporal properties of a Java class in an extension of JML (Java Modeling Language) called JTPL (Java Temporal Pattern Language). We particularly address the verification of liveness properties by automatically 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.

Domaines: Génie logiciel [cs.SE]; Modélisation et simulation

Julien Groslambert, Jacques Julliand, Olga Kouchnarenko. {JML}-based Verification of Liveness Properties on a Class in isolation. SAVCBS'06, Specification and Verification of Component-Based Systems, 2006, United States. pp.41--48. ⟨hal-00561442⟩