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, 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.
Type de document :
Communication dans un congrès
Helen Treharne, Steve King, Martin Henson and Steve Schneider. International Conference on Formal Specification and Development in Z and B - ZB'05, Apr 2005, Guildford, United Kingdom. Springer Berlin / Heidelberg, 3455, pp.434-453, 2005, Lecture Notes in Computer Science. 〈10.1007/b135596〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00329986
Contributeur : Frédéric Dadeau <>
Soumis le : lundi 13 octobre 2008 - 17:23:09
Dernière modification le : jeudi 15 février 2018 - 08:48:09

Identifiants

Citation

Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert. Checking JML Specifications with B Machines. Helen Treharne, Steve King, Martin Henson and Steve Schneider. International Conference on Formal Specification and Development in Z and B - ZB'05, Apr 2005, Guildford, United Kingdom. Springer Berlin / Heidelberg, 3455, pp.434-453, 2005, Lecture Notes in Computer Science. 〈10.1007/b135596〉. 〈inria-00329986〉

Partager

Métriques

Consultations de la notice

213