  We propose a verified approach to the formal verification of timed properties
using model-checking techniques. We focus on properties expressed using
real-time specification patterns, which can be viewed as a subset of timed
temporal logics that includes properties commonly found during the analysis of
reactive systems. Our model-checking approach is based on the use of observers
in order to transform the verification of timed patterns into the verification
of simpler LTL formulas. While the use of observers for model-checking is quite
common, our contribution is original in several ways. First, we define a formal
framework to verify that our observers are correct and non-intrusive. Second,
we define different classes of observers for each pattern and use a pragmatic
approach in order to select the most efficient candidate in practice. This
approach is implemented in an integrated verification tool chain for the Fiacre
language.
