|
|
|
Compositional encoding for bounded model checking |
| SUN Jun1, LIU Yang1, Dong Jin Song1, Sun Jing2 |
| 1.School of Computing, National University of Singapore; 2.epartment of Computer Science, The University of Auckland; |
|
|
|
|
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.
|
|
Issue Date: 05 December 2008
|
|
| 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: 1020 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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
