This paper presents a method for using timing assumptions to prove that an implementation meets a speed-independent specification. The approach is based on a continuous model of time, where times are real numbers, and it extends speed-independent verification methods for finite-state concurrent systems. The method associates each state with a convex linear region describing the possible states of individual timers, which are fictitious components tracking event occurrence times. This allows the method to handle liveness properties and indeterminate computations. The cost of the method is exponential in the number of timers and the size of the specification automaton. The paper discusses three categories of timing models: discrete-time models, continuous-time models with a global clock, and integer-bounded continuous-time models. The authors propose a new model that combines the advantages of these models, allowing flexible coupling between system events and timing constraints, and verifying general linear-time temporal properties. The framework for speed-independent verification is described using trace sets, where traces represent possible system histories. Properties are represented as trace sets, and a system satisfies a property if its trace set is a subset of the property's trace set. The paper also introduces the concept of timers, which are fictitious components that can be set to arbitrary real values within specified bounds. Timers are used to enforce timing constraints in the verification process. The paper defines a deterministic Büchi automaton that accepts timing-consistent traces, which are traces where the set and expire events occur in an order allowed by the timing constraints. The automaton is constructed by combining a well-formedness automaton and a timer region automaton. The well-formedness automaton accepts all well-formed traces, while the timer region automaton enforces ordering constraints between timer expirations. The paper also provides a finite representation of timer regions using difference bounds matrices (DB matrices), which are used to represent bounds on individual timer values and their differences. The canonical form of a DB matrix is determined by solving an all-pairs shortest path problem, ensuring unique representation for each region. Finally, the paper proves that the number of states in the timer region automaton is finite, bounded by the product of the upper bounds of the timers. This ensures that the verification process remains efficient despite the potentially large number of timer regions.This paper presents a method for using timing assumptions to prove that an implementation meets a speed-independent specification. The approach is based on a continuous model of time, where times are real numbers, and it extends speed-independent verification methods for finite-state concurrent systems. The method associates each state with a convex linear region describing the possible states of individual timers, which are fictitious components tracking event occurrence times. This allows the method to handle liveness properties and indeterminate computations. The cost of the method is exponential in the number of timers and the size of the specification automaton. The paper discusses three categories of timing models: discrete-time models, continuous-time models with a global clock, and integer-bounded continuous-time models. The authors propose a new model that combines the advantages of these models, allowing flexible coupling between system events and timing constraints, and verifying general linear-time temporal properties. The framework for speed-independent verification is described using trace sets, where traces represent possible system histories. Properties are represented as trace sets, and a system satisfies a property if its trace set is a subset of the property's trace set. The paper also introduces the concept of timers, which are fictitious components that can be set to arbitrary real values within specified bounds. Timers are used to enforce timing constraints in the verification process. The paper defines a deterministic Büchi automaton that accepts timing-consistent traces, which are traces where the set and expire events occur in an order allowed by the timing constraints. The automaton is constructed by combining a well-formedness automaton and a timer region automaton. The well-formedness automaton accepts all well-formed traces, while the timer region automaton enforces ordering constraints between timer expirations. The paper also provides a finite representation of timer regions using difference bounds matrices (DB matrices), which are used to represent bounds on individual timer values and their differences. The canonical form of a DB matrix is determined by solving an all-pairs shortest path problem, ensuring unique representation for each region. Finally, the paper proves that the number of states in the timer region automaton is finite, bounded by the product of the upper bounds of the timers. This ensures that the verification process remains efficient despite the potentially large number of timer regions.