Aspect-Oriented Model-Based Testing with UPPAAL Timed Automata

This paper presents a method for offline test derivation from formal aspect-oriented models so that the tests provide coverage in terms of aspects related metrics. A test purpose specification method in temporal logic TCTL is proposed that enables referring to the attributes of aspect models symbolically. The method is exemplified on a health monitoring system and the quantitative evidence of the advantages provided by the method are evaluated in terms of work effort put into the test development and by analytical reasoning on the complexity.