Advertisement

Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures

  • Farn Wang
  • Karsten Schmidt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)

Abstract

We formally define the model of software with pointer data structures. We developed symbolic algorithms for the manipulation of conditions and assignments with indirect operands for verification with BDD-like data-structures. We rely on two techniques, including inactive variable elimination and process-symmetry reduction in the data-structure configuration, to contain the time and memory complexity. We use binary permutation for efficiency but also identify the possibility of anomaly of image false reachability. We implemented the techniques in tool red and compare performance with Murø and SMC against several other benchmarks.

Keywords

Symmetry symbolic model-checking pointers datastructures 

References

  1. [1]
    R. Alur, C. Courcoubetis, D.L. Dill. Model Checking in Dense Real-Time, Information and Computation 104, pp.2–34 (1993).zbMATHCrossRefMathSciNetGoogle Scholar
  2. [2]
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond, IEEE LICS, 1990.Google Scholar
  3. [3]
    M. Bozga, C. Daws. O. Maler. Kronos: A model-checking tool for real-time systems. 10th CAV, June/July 1998, LNCS 1427, Springer-Verlag.Google Scholar
  4. [4]
    J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, Wang Yi. UPPAAL-a Tool Suite for Automatic Verification of Real-Time Systems. Hybrid Control System Symposium, 1996, LNCS, Springer-Verlag.Google Scholar
  5. [5]
    R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput., C-35(8), 1986.Google Scholar
  6. [6]
    E. Clarke, R. Enders, T. Filkorn, S. Jha. Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9, 77–104, 1996.CrossRefGoogle Scholar
  7. [7]
    D.L. Dill. The Murphi Verification System. CAV 1996, LNCS, Springer-Verlag.Google Scholar
  8. [8]
    E.A. Emerson, A.P. Sistla. Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach. ACM TOPLAS, Vol. 19, Nr. 4, July 1997, pp. 617–638.CrossRefGoogle Scholar
  9. [9]
    A.P. Sistla, V. Gyuris, E.A. Emerson. SMC: A Symmetry-based Model Checker for Verification of Safety and Liveness Properties. TOSEM 9(2): Pages 133–166Google Scholar
  10. [10]
    G.J. Holzmann. The Spin Model Checker, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279–295.CrossRefMathSciNetGoogle Scholar
  11. [11]
    C.N. Ip, D.L. Dill. Better Verification through Symmetry. FMSD 9(1/2):41–75, 1996.Google Scholar
  12. [12]
    J.M. Mellor-Crummey, M.L. Scott. “Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors.” ACM Transactions on Computer Systems, Vol. 9, No.1, Feb. 1991, pp.21–65.CrossRefGoogle Scholar
  13. [13]
    K. Schmidt. How to claculate symmetries of Petri nets. Acta Informatica 36, 545–590, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  14. [14]
    F. Wang. Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems. TACAS’2000, LNCS 1785, Springer-Verlag.Google Scholar
  15. [15]
    F. Wang. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram, IFIP FORTE, August 2001, Cheju Island, Korea.Google Scholar
  16. [16]
    F. Wang, P.-A. Hsiung. Efficient and User-Friendly Verification. IEEE Transactions on Computers, Jan. 2002, Vol. 51, Nr.1, ISSN 0018-9340, pp. 61–83. Preliminary materials of this paper also appears in proceedings of IEEE HASE’98, RTCSA’98, and IFIP FORTE’99.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Farn Wang
    • 1
  • Karsten Schmidt
    • 2
  1. 1.Inst. of Info. ScienceAcademia SinicaTaipei, TaiwanROC
  2. 2.Dept. of Computer ScienceCarnegie-Mellon UniversityPittsburgh, PAUSA

Personalised recommendations