Sciweavers

Share
ATVA
2006
Springer

Branching-Time Property Preservation Between Real-Time Systems

10 years 1 months ago
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.
Jinfeng Huang, Marc Geilen, Jeroen Voeten, Henk Co
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATVA
Authors Jinfeng Huang, Marc Geilen, Jeroen Voeten, Henk Corporaal
Comments (0)
books