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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071253
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 2:53:11 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM
Long-term archiving on : Sunday, April 4, 2010 - 10:04:44 PM

Identifiers

  • HAL Id : inria-00071253, version 1

Citation

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⟩

Share

Metrics

Record views

277

Files downloads

236