Branching-Time Property Preservation Between Real-Time Systems

In the past decades, many formal frameworks (e.g. timed automata and temporal logics) and techniques (e.g. model checking and theorem proving) have been proposed to model a real-time system and to analyze real-time properties of the model. However, due to the existence of ineliminable timing differences between the model and its realization, real-time properties verified in the model often cannot be preserved in its realization. In this paper, we propose a branching representation (timed state tree) to specify the timing behavior of a system, based on which we prove that real-time properties represented by Timed CTL (TCTL in short) formulas can be preserved between two neighboring real-time systems. This paper extends the results in [1][2], such that a larger scope of real-time properties can be preserved between real-time systems.

• Type: Conference
• Year: 2006
• Where: ATVA
• Authors: Jinfeng Huang, Marc Geilen, Jeroen Voeten, Henk Corporaal
• Keywords: ATVA 2006, Hardware, Model, Real-time Properties, Real-time Systems