Automatic generation of test data for extended finite state machine models based on Tabu search algorithm