This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures
January 2005 (vol. 31 no. 1)
pp. 38-51
Farn Wang, IEEE Computer Society
We introduce a new BDD-like data structure called Hybrid-Restriction Diagrams (HRDs) for the representation and manipulation of linear hybrid automata (LHA) state-spaces and present algorithms for weakest precondition calculations. This permits us to reason about the valuations of parameters that make safety properties satisfied. Advantages of our approach include the ability to represent discrete state information and concave polyhedra in a unified scheme, as well as to save both memory consumptions and manipulation times when processing the same substructures in state-space representations. Our experimental results document its efficiency in practice.

[1] A. Annichini, E. Asarin, and A. Bouajjani, “Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems,” Proc. Int'l Conf. Computer Aided Verification, 2000.
[2] E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, and A. Rasse, “Data-Structures for the Verification of Timed Automata,” Proc. Hybrid and Real-Time Systems Int'l Workshop, pp. 346-360, 1997.
[3] A. Annichini, A. Bouajjani, and M. Sighireanu, “TReX: A Tool for Reachability Analysis of Complex Systems,” Proc. 13th Int'l Conf. Computer Aided Verification, pp. 368-372, 2001.
[4] R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho, “Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems,” Proc. Hybrid Systems Workshop, pp. 209-229, 1993.
[5] R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, “The Algorithmic Analysis of Hybrid Systems,” Theoretical Computer Science, vol. 138, no. 1, pp. 3-34, 1995.
[6] R. Alur and D.L. Dill, “Automata for Modelling Real-Time Systems,” Proc. Int'l Colloquium on Automata, Languages and Programming, pp. 322-335, 1990.
[7] R. Alur, T.A. Henzinger, and P.-H. Ho, “Automatic Symbolic Verification of Embedded Systems,” Proc. IEEE Real-Time System Symp., pp. 2-11, 1993.
[8] R. Alur, T.A. Henzinger, and M.Y. Vardi, “Parametric Real-Time Reasoning,” Proc. 25th ACM Symp. Theory of Computing, pp. 592-601, 1993.
[9] F. Balarin, “Approximate Reachability Analysis of Timed Automata,” Proc. 17th IEEE Real-Time Systems Symp., p. 52, 1996.
[10] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, “Symbolic Model Checking: $10^{20}$ States and Beyond,” Proc. IEEE Symp. Logic in Computer Science, 1990.
[11] G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, and Wang Yi, “Efficient Timed Reachability Analysis Using Clock Difference Diagrams,” Proc. Int'l Conf. Computer Aided Verification, 1999.
[12] R.E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[13] D.L. Dill, “Timing Assumptions and Verification of Finite-State Concurrent Systems,” Proc. Int'l Conf. Computer Aided Verification, 1989.
[14] M. Fujita, H. Fujisawa, and Y. Matsunaga, “Variable Ordering Algorithms for Ordered Binary Decision Diagrams and Their Evaluation,” IEEE Trans. Computer-Aided Design, vol. 12, pp. 6-12, Jan. 1993.
[15] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, “HyTech: The Next Generation,” Proc. IEEE Real-Time Systems Symp., pp. 56-65, 1995.
[16] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic Model Checking for Real-Time Systems,” Proc. Seventh Symp. Logics in Computer Science, pp. 394-406, 1992.
[17] S. Minato, N. Ishiura, and S. Yajima, “Shared Binary Decision Diagram with Attributed Edges for Efficient Boolean Function Manipulation,” Proc. ACM/IEEE 27th Design Automation Conf., pp. 52-57, 1990.
[18] J. Moller, J. Lichtenberg, H.R. Andersen, and H. Hulgaard, “Difference Decision Diagrams,” Proc. Ann. Conf. European Assoc. for Computer Science Logic, Sept. 1999.
[19] S. Malik, A.R. Wang, R.K. Brayton, and A. Sangiovanni-Vincentelli, “Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment,” Proc. Int'l Conf. Computer-Aided Design, pp. 6-8, 1988.
[20] P. Pettersson and K.G. Larsen, “UPPAAL2k,” Bull. European Assoc. Theoretical Computer Science, vol. 70, pp. 40-44, 2000.
[21] F. Wang, “Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2000.
[22] F. Wang, “Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems,” Proc. 24th Int'l Computer Software and Applications Conf., Oct. 2000.
[23] F. Wang, “RED: Model-Checker for Timed Automata with Clock-Restriction Diagram,” Proc. Workshop Real-Time Tools, Technical Report 2001-014, ISSN 1404-3203, Dept. of Information Technology, Uppsala Univ., Aug. 2001.
[24] F. Wang, “Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram,” Proc. Int'l Conf. Formal Techniques for Networked and Distributed Systems, Aug. 2001.
[25] F. Wang, “Efficient Verification of Timed Automata with BDD-Like Data-Structures,” Proc. Int'l Conf. Verification, Model Checking and Abstract Interpretation, 2003.
[26] F. Wang, “Model-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptions,” Proc. 10th Int'l Conf. Algebraic Methodology and Software Technology, July 2004.
[27] F. Wang, G.-D. Hwang, and F. Yu, “TCTL Inevitability Analysis of Dense-Time Systems,” Proc. Eighth Conf. Implementation and Application of Automata, July 2003.
[28] F. Wang, G.-D. Hwang, and F. Yu, “Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems,” Proc. Int'l Conf. Formal Techniques for Networked and Distributed Systems, Sept.-Oct. 2003.
[29] F. Wang, A. Mok, and E.A. Emerson, “Symbolic Model-Checking for Distributed Real-Time Systems,” Proc. First Int'l Symp. Formal Methods Europe, Apr. 1993.
[30] H. Wong-Toi, “Symbolic Approximations for Verifying Real-Time Systems,” PhD thesis, Stanford Univ., 1995.
[31] S. Yovine, “Kronos: A Verification Tool for Real-Time Systems,” Int'l J. Software Tools for Technology Transfer, vol. 1, nos. 1-2, Oct. 1997.

Index Terms:
Data-structures, BDD, hybrid automata, verification, model-checking.
Citation:
Farn Wang, "Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures," IEEE Transactions on Software Engineering, vol. 31, no. 1, pp. 38-51, Jan. 2005, doi:10.1109/TSE.2005.13
Usage of this product signifies your acceptance of the Terms of Use.