TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering
Resource
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL. 28, NO. 7, JULY 2006
Journal
IEEE Transactions on Software Engineering
Journal Volume
VOL. 28
Journal Issue
NO. 7
Pages
510-526
Date Issued
2006-07
Date
2006-07
Author(s)
DOI
246246/200611150121460
Abstract
Inevitability properties in branching temporal logics are of the syntax 8} , where is an arbitrary (timed) CTL (Computation
Tree Logic) formula. Such inevitability properties in dense-time logics can be analyzed with the greatest fixpoint calculation. We
present algorithms to model-check inevitability properties. We discuss a technique for early decision on greatest fixpoint calculation
which has shown promising performance against several benchmarks. We have experimented with various issues which may affect
the performance of TCTL inevitability analysis. Specifically, our algorithms come with a parameter for the measurement of timeprogress.
We report the performance of our implementation with regard to various parameter values and with or without the non-Zeno
computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstraction techniques for
model-checking TCTL inevitability properties. The experiment results help us in deducing rules for setting the parameter for verification
performance. Finally, we summarize suggestions for configurations of efficient TCTL inevitability evaluation procedure.
Subjects
TCTL
real-time systems
inevitability
non-Zeno
model-checking
greatest fixpoint
abstraction
Publisher
Taipei:National Taiwan University Dept Mech Engn
Type
journal article
File(s)![Thumbnail Image]()
Loading...
Name
555.pdf
Size
3.99 MB
Format
Adobe PDF
Checksum
(MD5):abf03e85bc000dbb798d0734643fdc6f