Symbolic Animation of JML Specifications

Fabrice Bouquet 1 Frédéric Dadeau 1 Bruno Legeard 1 Marc Utting 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 model-based framework for the symbolic animation of object-oriented specifications. A customized set-theoretic solver is used to simulate the execution of the system and handle constraints on state variables. We define a framework for animating object-oriented specifications with dynamic object creations, interactions and inheritance. We show how this technique can be applied to Java Modeling Language (JML) specifications, making it possible to animate Java programs that only contain method interfaces and no code!
Type de document :
Communication dans un congrès
John Fitzgerald, Ian J. Hayes and Andrzej Tarlecki. International Conference on Formal Methods - FM'05, Jul 2005, Newcastle upon Tyne, United Kingdom. Springer Berlin / Heidelberg, 3582, pp.75-90, 2005, Lecture Notes in Computer Science. 〈10.1007/b27882〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00329983
Contributeur : Frédéric Dadeau <>
Soumis le : lundi 13 octobre 2008 - 17:20:18
Dernière modification le : jeudi 11 janvier 2018 - 06:20:00

Identifiants

Citation

Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Marc Utting. Symbolic Animation of JML Specifications. John Fitzgerald, Ian J. Hayes and Andrzej Tarlecki. International Conference on Formal Methods - FM'05, Jul 2005, Newcastle upon Tyne, United Kingdom. Springer Berlin / Heidelberg, 3582, pp.75-90, 2005, Lecture Notes in Computer Science. 〈10.1007/b27882〉. 〈inria-00329983〉

Partager

Métriques

Consultations de la notice

178