Branching-time property preservation between real-time systems
conference paper
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.
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.
Topics
TNO Identifier
953851
ISSN
03029743
ISBN
3540472371
Publisher
Springer Verlag
Source title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006, 23 October 2006 through 26 October 2006
Pages
260-275
Files
To receive the publication files, please send an e-mail request to TNO Repository.