Abstract:

Model Based Testing for Real-The Inhouse Card Case Study

A. Pretschner and O. Slotosch and E. Aiglstorfer and S. Kriebel


Model-based testing relies on abstract behavior models for test case generation. These models are abstractions, 
i.e., simplifications. For deterministic reactive systems, test cases are sequences of input and expected output. In 
order to bridge the different levels of abstraction, input must be concretized before being applied to the system 
under test. The system's output must then be abstracted before being compared to the output of the model.The 
concepts are discussed along the lines of a feasibility study, an inhouse smart card case study. We describe the 
modeling concepts of the CASE tool AutoFocus and an approach to model-based test case generation that is 
based on symbolic execution with Constraint Logic Programming.Different search strategies and algorithms for 
test case generation are discussed. Besides validating the model itself, generated test cases were used to verify 
the actual hardware w.r.t. these traces.