Checking JML Specifications with B Machines

Fabrice Bouquet 1 Frédéric Dadeau 1 Julien Groslambert 2
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
Abstract : This paper presents a solution to the lack of tool-support for the JML models verification. We propose an approach for expressing JML specifications within the B abstract machines notation. The B machines generated from the JML can then be checked to ensure their correctness. Thus, we deduce the correctness of the original JML specification, ensured by rewriting rules which give the semantical equivalence of the two models. More generally, this translation can be applied to object-oriented specification languages using before-after predicates.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00329986
Contributor : Frédéric Dadeau <>
Submitted on : Monday, October 13, 2008 - 5:23:09 PM
Last modification on : Friday, July 6, 2018 - 3:06:09 PM

Identifiers

Citation

Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert. Checking JML Specifications with B Machines. International Conference on Formal Specification and Development in Z and B - ZB'05, Apr 2005, Guildford, United Kingdom. pp.434-453, ⟨10.1007/b135596⟩. ⟨inria-00329986⟩

Share

Metrics

Record views

244