An Abstract Interpretation Framework for Diagnosis and Verification of Timed Concurrent Constraint Languages