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
2 EVEREST - Environments for Verification and Security of Software

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.

Mots clés: verification; liveness; jml

Domaines: Autre [cs.OH]

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⟩