Book chapter
Symbolic animation of JML specifications
FM 2005: Formal Methods, pp.75-90
Formal Methods Europe (FME) International Symposium, 2005 (Newcastle, United Kingdom, 18-Jul-2005–22-Jul-2005)
Lecture Notes in Computer Science (LNCS), 3582, Springer Berlin Heidelberg
2005
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! ©Springer-Verlag Berlin Heidelberg 2005.
Details
- Title
- Symbolic animation of JML specifications
- Authors
- Fabrice Bouquet (Author) - Université de Franche-Comté, FranceFrederic Dadeau (Author) - Université de Franche-Comté, FranceBruno Legeard (Author) - Université de Franche-Comté, FranceMark Utting (Author) - Université de Franche-Comté, France
- Contributors
- J Fitzgerald (Editor)I J Hayes (Editor)A Tarlecki (Editor)
- Publication details
- FM 2005: Formal Methods, pp.75-90
- Conference details
- Formal Methods Europe (FME) International Symposium, 2005 (Newcastle, United Kingdom, 18-Jul-2005–22-Jul-2005)
- Series
- Lecture Notes in Computer Science (LNCS); 3582
- Publisher
- Springer Berlin Heidelberg
- Date published
- 2005
- DOI
- 10.1007/11526841_7
- ISBN
- 9783540278825
- Organisation Unit
- School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
- Language
- English
- Record Identifier
- 99448882602621
- Output Type
- Book chapter
Metrics
2 File views/ downloads
545 Record Views