Ernits, JuhanKull, AndreasRaiend, KulloVain, JüriHochberger, ChristianLiskowsky, Rüdiger2019-06-042019-06-042006978-3-88579-188-1https://dl.gi.de/handle/20.500.12116/23518The paper describes a full procedure of executable test code generation from specification models using the Uppaal model checker. Test cases are generated for black-box testing of reactive software that is connected to the tester via an asynchronous message-based interface. For specifying the observable behaviour of the software under test we define a modelling language that is based on extended finite state machines. A model in such a language is transformed to a Uppaal model taking a structural coverage criterion as a parameter. Uppaal is used to find an abstract test sequence that is suboptimal in terms of length. Next, we present the rules for transforming the abstract test sequences to TTCN-3.enText/Conference Paper1617-5468