My research area is fundamental of formal analysis of real-time embedded systems. The main objective of this research is the theoretical and practical development of a verification algorithm for the formal analysis of real-time embedded systems based on the combination of real-time model checking and abstract interpretation of real-time models. The objective of the proposed combination is an improved behavior both in time and space requirement of the resulting algorithm. One of drawbacks of all current real-time model-checking tools is the limited size of the systems that can be analyzed. By combination of state-space exploration with abstract interpretation we expect to scale up the size of applications