TA Splitting for Reachability Testing Reachability testing in timed automata using pseudo-simulating abstract model generated on-the-fly and using zone splitting and DBMs