This paper describes the automated generation of test sequences derived from a JML specification and a safety property written in an ad hoc language, named JTPL. The functional JML model is animated to build the test sequences w.r.t. the safety properties, which represent the test targets. From these properties, we derive strategies that are used to guide the symbolic animation. Moreover, additional JML annotations reinforce the oracle in order to guarantee that the safety properties are not violated during the execution of the test suite. Finally, we illustrate this approach on an industrial JavaCard case study. © 2006 Springer-Verlag Berlin/Heidelberg.
CITATION STYLE
Bouquet, F., Dadeau, F., Groslambert, J., & Julliand, J. (2006). Safety property driven test generation from JML specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4262 LNCS, pp. 225–239). Springer Verlag. https://doi.org/10.1007/11940197_15
Mendeley helps you to discover research relevant for your work.