This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering
July 2006 (vol. 32 no. 7)
pp. 510-526
ASCII Text
x 
 
Farn Wang, Geng-Dian Huang, Fang Yu, "TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering," IEEE Transactions on Software Engineering, vol. 32, no. 7, pp. 510-526, July, 2006.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2006.71,
author = {Farn Wang and Geng-Dian Huang and Fang Yu},
title = {TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering},
journal ={IEEE Transactions on Software Engineering},
volume = {32},
number = {7},
issn = {0098-5589},
year = {2006},
pages = {510-526},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2006.71},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering
IS - 7
SN - 0098-5589
SP510
EP526
EPD - 510-526
A1 - Farn Wang,
A1 - Geng-Dian Huang,
A1 - Fang Yu,
PY - 2006
KW - TCTL
KW - real-time systems
KW - inevitability
KW - non-Zeno
KW - model-checking
KW - greatest fixpoint
KW - abstraction.
VL - 32
JA - IEEE Transactions on Software Engineering
ER -
 
Farn Wang, IEEE Computer Society
Inevitability properties in branching temporal logics are of the syntax \forall\diamondsuit \phi, where \phi 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 time-progress. 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.

[1] R. Alur, C. Courcoubetis, and D.L. Dill, “Model Checking for Real-Time Systems,” Proc. IEEE Fifth Symp. Logic in Computer Science, pp. 414-425, 1990.
[2] R. Alur and D.L. Dill, “Automata for Modeling Real-Time Systems,” Proc. Int'l Colloquium Automata, Languages, and Programming, pp. 322-335, 1990.
[3] B. Alpern and F.B. Schneider, “Defining Liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181-185, 1985.
[4] F. Balarin, “Approximate Reachability Analysis of Timed Automata,” Proc. IEEE Real-Time Systems Symp., pp. 52-61, 1996.
[5] G. Behrmann, P. Bouyer, K.G. Larsen, and R. Pelanek, “Lower and Upper Bounds in Zone Based Abstractions of Timed Automata,” Proc. 10th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 312-326, 2004.
[6] G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, and W. Yi, “Efficient Timed Reachability Analysis Using Clock Difference Diagrams,” Proc. 11th Int'l Conf. Computer-Aided Verification, pp. 341-353, 1999.
[7] S.V. Campos, “A Quantitative Approach to the Formal Verification of Real-Time Systems,” PhD Thesis, Carnegie Mellon Univ., 1996.
[8] E.M. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 2000.
[9] P. Cousot and R. Cousot, “Abstract Interpretation and Application to Logic Programs,” J. Logic Programming, vol. 13, no. 2-3, pp. 103-179, 1992.
[10] E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal-Logic Specifications,” ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[11] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-Guided Abstraction Refinement,” Proc. 12th Int'l Conf. Computer-Aided Verification, pp. 154-169, 2000.
[12] D.L. Dill, “Timing Assumptions and Verification of Finite-State Concurrent Systems,” Proc. Int'l Workshop Automatic Verification Methods for Finite State Systems, pp. 197-212, 1989.
[13] C. Daws, A. Olivero, S. Tripakis, and S. Yovine, “The Tool KRONOS,” Proc. Third Hybrid Systems, pp. 208-219, 1996.
[14] E.A. Emerson, “Uniform Inevitability Is Tree Automation Ineffable,” Information Processing Letters, vol. 24, no. 2, pp. 77-79, 1987.
[15] B.C. Eaves and U.G. Rothblum, “Dines-Fourier-Motzkin Quantifier Elimination and an Application of Corresponding Transfer Principles over Ordered Fields,” Math. Programming, vol. 53, no. 3, pp. 307-321, 1992.
[16] J. Haartsen, “Bluetooth Baseband Specification, version 1.0,” http:/www.bluetooth.com/, 2006.
[17] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic Model Checking for Real-Time Systems, ” Proc. IEEE Seventh Symp. Logic in Computer Science, pp. 394-406, 1992.
[18] P.-A. Hsiung and F. Wang, “User-Friendly Verification,” Proc. IFIP Joint Int'l Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification, pp. 279-294, 1999.
[19] F. Laroussinie and K.G. Larsen, “CMC: A Tool for Compositional Model-Checking of Real-Time Systems,” Proc. IFIP Joint Int'l Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification, pp. 439-456, 1998.
[20] J. Moller, J. Lichtenberg, H.R. Andersen, and H. Hulgaard, “Difference Decision Diagrams,” Proc. Ann. Conf. European Assoc. for Computer Science Logic, pp. 111-125, 1999.
[21] M.O. Moller, “Parking Can Get You There Faster— Model Augmentation to Speed Up Real-Time Model Checking,” Electronic Notes in Theoretical Computer Science, vol. 65, no. 6, 2002.
[22] A.W. Mazurkiewicz, E. Ochmanski, and W. Penczek, “Concurrent Systems and Inevitability,” Theoretical Computer Science, vol. 64, no. 3, pp. 281-304, 1989.
[23] I. Ober, S. Graf, and I. Ober, “Validation of UML Models via a Mapping to Communicating Extended Timed Automata,” Proc. 11th Int'l SPIN Workshop Model Checking of Software, pp. 127-145, 2004.
[24] P. Pettersson and K.G. Larsen, “UPPAAL2k,” Bull. European Assoc. Theoretical Computer Science, vol. 70, pp. 40-44, 2000.
[25] R.S. Pressman, Software Engineering, a Practitioner's Approach. McGraw-Hill, 1982.
[26] F. Wang, “Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems,” Proc. Sixth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 157-171, 2000.
[27] F. Wang, “Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems,” Proc. 24th IEEE Computer Software and Applications Conf., pp. 509-515, 2000.
[28] F. Wang, “RED: Model-Checker for Timed Automata with Clock-Restriction Diagram,” Proc. Workshop Real-Time Tools, Technical Report 2001-014, Dept. of Information Technology, Uppsala Univ., Aug. 2001.
[29] F. Wang, “Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram,” Proc. 21st IFIP Int'l Conf. Formal Techniques for Networked and Distributed Systems, pp. 235-250, 2001.
[30] F. Wang, “Efficient Verification of Timed Automata with BDD-Like Data-Structures,” Proc. Fourth Int'l Conf. Verification, Model Checking, and Abstract Interpretation, pp. 189-205, 2003.
[31] F. Wang and P.-A. Hsiung, “Automatic Verification on the Large,” Proc. Third IEEE Int'l Symp. High-Assurance Systems Eng., pp. 134-141, 1998.
[32] F. Wang and P.-A. Hsiung, “Efficient and User-Friendly Verification,” IEEE Trans. Computers, vol. 51, no. 1, pp. 61-83, Jan. 2002.
[33] F. Wang and F. Yu, “OVL Assertion-Checking of Embedded Software with Dense-Time Semantics,” Proc. Ninth Int'l Conf. Real-Time and Embedded Computing Systems and Applications, pp. 254-278, 2003.
[34] F. Wang, G.-D. Hwang, and F. Yu, “Symbolic Simulation of Real-Time Concurrent Systems,” Proc. Ninth Int'l Conf. Real-Time and Embedded Computing Systems and Applications, pp. 595-617, 2003.
[35] H. Wong-Toi, “Symbolic Approximations for Verifying Real-Time Systems,” PhD thesis, Stanford Univ., 1995.
[36] S. Yovine, “Kronos: A Verification Tool for Real-Time Systems,” Int'l J. Software Tools for Technology Transfer, vol. 1, nos. 1-2, 1997.

Index Terms:
TCTL, real-time systems, inevitability, non-Zeno, model-checking, greatest fixpoint, abstraction.
Citation:
Farn Wang, Geng-Dian Huang, Fang Yu, "TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering," IEEE Transactions on Software Engineering, vol. 32, no. 7, pp. 510-526, July 2006, doi:10.1109/TSE.2006.71
Usage of this product signifies your acceptance of the Terms of Use.