• Publication
  • 2004
  • Issue No. 6 - June
  • Abstract - BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction
June 2004 (vol. 30 no. 6)
pp. 403-417

Abstract—Dynamic data-structures with pointer links, which are heavily used in real-world software, cause extremely difficult verification problems. Currently, there is no practical framework for the efficient verification of such software systems. We investigated symmetry reduction techniques for the verification of software systems with C-like indirect reference chains like x->y->z->w. We formally defined the model of software with pointer data structures and developed symbolic algorithms to manipulate conditions and assignments with indirect reference chains using BDD technology. We relied on two techniques, inactive variable elimination and process-symmetry reduction in the data-structure configuration, to reduce time and memory complexity. We used binary permutation for efficiency, but we also identified the possibility of an anomaly of false image reachability. We implemented the techniques in tool Red 5.0 and compared performance with Murø and SMC against several benchmarks.

[1] R. Alur, C. Courcoubetis, and D.L. Dill, Model Checking in Dense Real-Time Information and Computation, vol. 104, pp. 2-34, 1993.
[2] M.C. Browne, E.M. Clarke, and O. Grumberg, Reasoning about Networks with Many Finite Processes Proc. Fifth ACM Symp. Principles of Distributed Computing, pp. 240-248, 1986.
[3] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: 1020States and Beyond," Proc. IEEE Symp. Logic in Computer Science, pp. 428-439, 1990.
[4] M. Bozga, C. Daws, and O. Maler, Kronos: A Model-Checking Tool for Real-Time Systems Proc. 10th Conf. Computer-Aided Verification, June/July 1998.
[5] J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, and W. Yi, UPPAAL A Tool Suite for Automatic Verification of Real-Time Systems Proc. Hybrid Control System Symp., 1996.
[6] R.E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation IEEE Trans. Computers, vol. 35, no. 8, Aug. 1986.
[7] P. Cousot and R. Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints Proc. Fourth Ann. Symp. Principles of Programming Languages, 1977.
[8] E. Clarke and E.A. Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic Proc. Workshop Logic of Programs, 1981.
[9] E. Clarke, R. Enders, T. Filkorn, and S. Jha, Exploiting Symmetry in Temporal Logic Model Checking Formal Methods in System Design, vol. 9, pp. 77-104, 1996.
[10] E.M. Clarke, O. Grumberg, and S. Jha, Verifying Parameterized Networks Using Abstraction and Regular Languages Proc. Sixth Int'l Conf. Concurrency Theory, pp. 395-407, Aug. 1995.
[11] D.L. Dill, The Murphi Verification System Proc. Computer-Aided Verification Conf., 1996.
[12] A.P. Sistla, V. Gyuris, and E. A. Emerson, SMC: A Symmetry-Based Model Checker for Verification of Safety and Liveness Properties ACM Trans. Software Eng. Methods, vol. 9, no. 2, pp. 133-166, 2000.
[13] E.A. Emerson and K.S. Namjoshi, Reasoning about Rings Proc. 22th ACM Symp. Principles of Programming Languages, 1995.
[14] E.A. Emerson and A.P. Sistla, Symmetry and Model Checking Formal Methods in System Design: An Int'l J., vol. 9, no. 1, pp 105-131, Aug. 1996.
[15] E.A. Emerson and A.P. Sistla, Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach ACM Trans. Programming Languages and Systems, vol. 19, no. 4, pp. 617-638, July 1997.
[16] P. Godefroid, Using Partial Orders to Improve Automatic Verification Methods Proc. Computer Aided Verification Workshop, 1990.
[17] G. Holzmann, P. Godefroid, and D. Pirottin, Coverage Preserving Reduction Strategies for Reachability Analysis Proc. 12th Int'l Symp. Protocol Specification, Testing, and Verification (PSTV), June 1992.
[18] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[19] G.J. Holzmann and D. Peled, An Improvement in Formal Verification Proc. Formal Techniques for Networked and Distributed Systems Conf., 1994.
[20] C.N. Ip and D.L. Dill, Better Verification through Symmetry Formal Methods in System Design J., vol. 9, nos. 1-2, pp. 41-75, 1996.
[21] R.P. Kurshan and K. McMillan, A Structural Induction Theorem for Processes Proc. Eighth ACM Symp. Principles of Distributed Computing, pp. 239-248, 1989.
[22] S. Katz and D.A. Peled, Verification of Distributed Programs Using Representative Interleaving Sequences Distributed Computing, vol. 6, pp 107-120, 1992.
[23] J.M. Mellor-Crummey and M.L. Scott, Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors ACM Trans. Computer Systems, vol. 9, no. 1, pp. 21-65, Feb. 1991.
[24] M.B. Dwyer, J. Hatcliff, and R. Iosif, Space-Reduction Strategies for Model Checking Dynamic Software Electronic Notes in Theoretical Computer Science, vol. 89, no. 3, 2003.
[25] K. Schmidt, How to Calculate Symmetries of Petri Nets Acta Informatica, vol. 36, pp. 545-590, 2000.
[26] A.P. Sistla and S.M. German, Reasoning about Systems with Many Processes J. ACM, vol. 30, pp. 675-735, 1992.
[27] A.P. Sistla, Parameterized Verification of Linear Networks Using Automata as Invariants Proc. Conf. Computer-Aided Verification, 1997.
[28] A. Silberschatz, P.B. Galvin, and G. Gagne, Operating System Concepts. John Wiley&Sons, 2003.
[29] F. Wang, Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems Proc. Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2000.
[30] 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.
[31] F. Wang, Symmetric Model-Checking of Concurrent Timed Automata with Clock-Restriction Diagram Proc. Int'l Workshop Real-Time Computing Systems and Applications, 2002.
[32] F. Wang and P.-A. Hsiung, Efficient and User-Friendly Verification IEEE Trans. Computers, vol. 51, no. 1, pp. 61-83, Jan. 2002.

Index Terms:
Symbolic model checking, pointers, data structure, address manipulation, symmetry reduction, experiments.
Citation:
Farn Wang, Karsten Schmidt, Fang Yu, Geng-Dian Huang, Bow-Yaw Wang, "BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction," IEEE Transactions on Software Engineering, vol. 30, no. 6, pp. 403-417, June 2004, doi:10.1109/TSE.2004.15
Usage of this product signifies your acceptance of the Terms of Use.