Test specification patterns for automatic generation of test sequences

Model Based Testing (MBT) enables automatic generation of test cases using models to specify the system behavior and requirements. Key features of MBT approaches are the automation level and the complexity of non-automated steps. Usually, test case generation is supported by some automatic technique whereas modeling is manually performed. UML statecharts or other extended finite state machine formalisms are widely used to build behavior models. To ease their development, as well as the extraction of test cases from them, is an important aspect to be addressed in order to perform testing activities with lower skill, cost and effort. This paper aims at providing a contribution to both the issues. Test Specification Patterns (TSPs) are proposed and expressed by means of UML annotated statecharts as a mean to aid the construction of models and build specifications on the base of well known recurring problems and their solutions (patterns). In order to improve usability and increase the automation level, a transformational approach is defined which derives Promela code from specifications built by TSPs composition and applies model checking to obtain test sequences by using the SPIN model checker. The usage of TSPs and the test case generation process is illustrated on a test scenario from the Radio Block Centre, the vital core of the modern railway control systems. © 2014 Springer International Publishing