Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Verification of Liveness Properties with JML

Françoise Bellegarde 1 Julien Groslambert 2 Marieke Huisman 2 Jacques Julliand 2 Olga Kouchnarenko 1 
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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper proposes a way to verify liveness properties in an extension of JML. The verification is divided into two subtasks: (1) generation of appropriate JML annotations that allow to verify that the class under consideration respects the liveness property, and (2) showing that the environment preserves the liveness properties by proving a refinement. For the generation of appropriate JML annotations, we require that the liveness properties are extended with a variant and invariant (conform variants and invariants to show termination of loops). We then show that under certain assumptions on the environment, we can prove the satisfaction of the liveness property. The second subtask then boils down to showing that the environment in fact respects these assumptions. The method is illustrated by an example.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 2:53:11 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:21 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:04:44 PM


  • HAL Id : inria-00071253, version 1


Françoise Bellegarde, Julien Groslambert, Marieke Huisman, Jacques Julliand, Olga Kouchnarenko. Verification of Liveness Properties with JML. [Research Report] RR-5331, INRIA. 2004, pp.24. ⟨inria-00071253⟩



Record views


Files downloads