Real-time property preservation in approximations of timed systems

Formal techniques have been widely applied in the design of real-time systems and have significantly helped detect design errors by checking real-time properties of the model. However, a model is only an approximation of its realization in terms of the issuing time of events. Therefore, a real-time property verified in the model can not always be directly transferred to the realization. In this paper, both the model and the realization are viewed as sets of timed state sequences. In this context, we first investigate the real-time property preservation between two neighboring timed state sequences (execution traces of timed systems), and then extend the results to two "neighboring" timed systems. The study of real-time property preservation gives insight in building a formal link between real-time properties satisfied in the model and those in the realization.