Automated test generation from formal specifications of real-time reactive systems