Towards the exhaustive verification of real-time aspects in controller implementation