Compositional encoding for bounded model checking

Abstract

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit on-the-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.

References

1. Clarke E M, Grumberg O, Peled D A . Model Checking. The MassachusettsInstitute of Technology(MIT) Press, 2000
2. Burch J R, Clarke E M, McMillan K L, et al.. Sequential circuit verification using symbolicmodel checking. In: Proceesings of 27thAssociation for Computing Machinery (ACM)/IEEE Design Automation Conference(DAC'90). Florida, 1990, 46–51
3. Biere A, Clarke E M, Raimi R, et al.. Verifiying safety properties of a Power PC microprocessorusing symbolic model checking without BDDs. In: Proceesings of 11th Inter. Conf. on Computer Aided Verification (CAV'99).Springer, 1999, 60–71
4. Alur R, Jagadeesan L J, Kott J J, et al.. Model-checking of real-time systems: a telecommunicationsapplication (experience report). In: Proceesingsof 19th International Conference on Software Engineering (ICSE'97),ACM, 1997, 514–524
5. Burch J R, Clarke E M, McMillan K L, et al.. Symbolic model checking: 10²⁰ states and beyond. Information and Computation, 1992, 98(2): 142–170. doi:10.1016/0890-5401(92)90017-A
6. Campos S V A, Clarke E M, Minea M . Symbolic techniques for formally verifying industrialsystems. Science of Computer Programming, 1997, 29(1–2): 79–98. doi:10.1016/S0167-6423(96)00030-5
7. Bryant R E . Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, 35(8): 677–691. doi:10.1109/TC.1986.1676819
8. Clarke E M, Biere A, Raimi R, et al.. Bounded model checking using satisfiabilitysolving. Formal Methods in System Design, 2001, 19(1): 7–34. doi:10.1023/A:1011276507260
9. SAT Competition. http://www.satcompetition.org/
10. Hoare C A R . Communicating sequential processes. InternationalSeries in Computer Science, Prentice-Hall, 1985
11. Cimatti A, Clarke E M, Giunchiglia E, et al.. NuSMV 2: an openSource tool for symbolic modelchecking. In: Proceesings of 14th InternationalConference on Computer Aided Verification (CAV 2002), 2002, 359–364
12. Brookes S D, Roscoe A W, Walker D J . An operational semantics for CSP Oxford University, Technical report, 1986
13. Roscoe A W . The theory and practice of concurrency, Prentice-Hall, 1997
14. Sun J, Liu Y, Dong J S . PAT: process analysis toolkit. http://pat.comp.nus.edu.sg, 2007
15. Chaki S, Clarke E M, Ouaknine J, et al.. State/event-based software model checking. In: Proceesings of 4th International Conferenceon Integrated Formal Methods (IFM 2004), 2004, 128–147
16. Gastin P and Oddoux D . Fast LTL to büchi automatatranslation. In: Proceesings of 13th InternationalConference on Computer Aided Verification (CAV 2001). Springer, 2001, 53–65
17. Holzmann G J . The model checker SPIN. IEEE Transactionson Software Engineering, 1997, 23(5): 279–295. doi:10.1109/32.588521
18. Sun J, Liu Y, Dong J S, et al.. Specifying and verifying event-based fairnessenhanced systems. In: Proceesings of 10thInternational Conference on Formal Engineering Methods (ICFEM 2008), 2008
19. Lamport L . Fairnessand hyperfairness. Distributed Computing, 2000, 13(4):239–245. doi:10.1007/PL00008921
20. Strichman O . Acceleratingbounded model checking of safety properties. Formal Methods in System Design, 2004, 24(1): 5–24. doi:10.1023/B:FORM.0000004785.67232.f8
21. Zhang W H . SAT-based verification of LTL formulas. In: Proceesings of 11th International Workshop FMICS 2006, 2006, 277–292
22. Armando A, Mantovani J, Platania L . Bounded model checking of software using SMT solversinstead of SAT solvers. In: Proceesingsof 13th Inte. SPIN Workshop on Model Checking Software (SPIN 2006), 2006, 146–162
23. Parashkevov A, Yantchev J . ARC - a tool for efficientrefinement and equivalence checking for CSP. In: Proceesings of the IEEE International Conference on Algorithms andArchitectures for Parallel Processing (ICA3PP '96), 1996, 68–75
24. Brooke P . Atimed semantics for a hierarchical design notation, PhD thesis, University of York, 1999
25. Dong J S, Hao P, Qin S C, et al.. Timed patterns: TCOZ to timed automata. In: Proceesings of 6th International Conferenceon Formal Engineering Methods (ICFEM 2004). Springer, 2004, 483–498
26. Dong J S, Hao P, Sun J, et al.. A reasoning method for timed CSP based on constraintsolving. In: Proceesings of 8th InternationalConference on Formal Engineering Methods (ICFEM 2006). Springer, 2006, 342–359
27. Dong J S, Liu Y, Sun J, et al.. Verification of computation orchestration viatimed automata. In: Proceesings of 8thInternational Conference on Formal Engineering Methods (ICFEM 2006), 2006, 226–245
28. Sun J, Dong J S . Design synthesis from interactionand state-based specifications. IEEE Transactionson Software Engineering, 2006, 32(6): 349–364. doi:10.1109/TSE.2006.55
29. Biere A, Cimatti A, Clarke E M, et al.. Symbolic model checking without BDDs. In: Proceesings of 5th International Conferenceon Tools and Algorithms for Construction and Analysis of Systems (TACAS'99).Springer, 1999, 193–207
30. Bryant R E, Lahiri S K, Seshia S A . Convergence testing in term-level bounded model checking. In: Proceesings of 12th IFIP WG 10.5 Advanced ResearchWorking Conference on Correct Hardware Design and Verification Methods(CHARME 2003), 2003, 348–362