Model checking techniques based on automata theory play a central role in formal verification. Nevertheless, classical automata are not composable for temporal operators, such that the model checking algorithms for various temporal logics cannot be organically integrated. To realize efficient model checking for real-time branching-time temporal logic RTCTL^* integrating bounded temporal operators, a construction method is proposed for RTCTL^* positive temporal testers, and the RTCTL^* symbolic model checking algorithm is further proposed based on positive temporal testers. It is proved that the proposed construction method for RTCTL^* positive temporal testers is complete. It is also proved that the time complexity of the proposed algorithm is linear in the size of the verified system and exponential in the length of the given formula. Based on the JavaBDD software package, the model checking tool MCTK 2.0.0 is successfully developed for the proposed algorithm. The experimental data and the analysis results show that although MCTK consumes more memory than the famous symbolic model checker nuXmv, the time complexity of MCTK is doubly-exponentially less than nuXmv, which makes it possible to verify real-time temporal properties of large-scale systems by MCTK.