Generating tests from B specifications and dynamic selection criteria |
| |
Authors: | Jacques Julliand Pierre-Alain Masson R��gis Tissot Pierre-Christophe Bu�� |
| |
Affiliation: | 1. LIFC, Universit?? de Franche-Comt??, 16, route de Gray, 25030, Besan?on Cedex, France
|
| |
Abstract: | This paper is about generating tests from dynamic selection criteria called test purposes, in addition to structural tests,
obtained from static selection criteria. We present a method that re-uses a behavioral 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 Leirios Test Generator (LTG) based on constraint solving,
and guided by the test purposes. We build for that a B model that is the synchronized product of a behavioral B abstract model
and a test purpose described as a labeled transition system. We prove the correctness of this method, and show some experimental
results obtained on the IAS case study. IAS is an industrial smart-card platform dedicated to the operations of Identification,
Authentication and electronic Signature. Our experiments show that the tests obtained from test purposes are complementary
to the structural tests. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|