This paper is about generating tests from test purposes, in addition to structural tests. We present a method that re-uses a behavioural model and an abstract test concretization layer developed for structural testing, and relies on additional test purposes. We propose, in the B framework, a process of test generation that uses the symbolic animation mechanisms of LTG (Leirios Test Generator) based on constraint solving, and guided by the test purposes. We build for that a B animable model that is the synchronized product of a behavioural B abstract model and a test purpose described as a labelled transition system. We prove the correctness of this method, and illustrate it by means of the IAS case study. IAS is a smart-card application dedicated to the operations of Identification, Authentication and electronic Signature.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{JulliandMT08,
author = {Jacques Julliand and
Pierre{-}Alain Masson and
R{\'{e}}gis Tissot},
editor = {Egon B{\"{o}}rger and
Michael J. Butler and
Jonathan P. Bowen and
Paul Boca},
title = {Generating Tests from {B} Specifications and Test Purposes},
booktitle = {Abstract State Machines, {B} and Z, First International Conference,
{ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5238},
pages = {139--152},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87603-8\_12},
doi = {10.1007/978-3-540-87603-8\_12},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/JulliandMT08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}