headerpos: 12198
 
 
 

Proceedings of the Estonian Academy of Sciences

ISSN 1736-7530 (electronic)   ISSN 1736-6046 (print)
Formerly: Proceedings of the Estonian Academy of Sciences, series Physics & Mathematics and  Chemistry
Published since 1952

Proceedings of the Estonian Academy of Sciences

ISSN 1736-7530 (electronic)   ISSN 1736-6046 (print)
Formerly: Proceedings of the Estonian Academy of Sciences, series Physics & Mathematics and  Chemistry
Published since 1952
Publisher
Journal Information
» Editorial Board
» Editorial Policy
» Archival Policy
» Article Publication Charges
» Copyright and Licensing Policy
Guidelines for Authors
» For Authors
» Instructions to Authors
» LaTex style files
Guidelines for Reviewers
» For Reviewers
» Review Form
Open Access
List of Issues
» 2020
» 2019
» 2018
» 2017
» 2016
» 2015
» 2014
» 2013
Vol. 62, Issue 4
Vol. 62, Issue 3
Vol. 62, Issue 2
Vol. 62, Issue 1
» 2012
» 2011
» 2010
» 2009
» 2008
» Back Issues Phys. Math.
» Back Issues Chemistry
» Back issues (full texts)
  in Google. Phys. Math.
» Back issues (full texts)
  in Google. Chemistry
» Back issues (full texts)
  in Google Engineering
» Back issues (full texts)
  in Google Ecology
» Back issues in ETERA Füüsika, Matemaatika jt
Subscription Information
Internet Links
Support & Contact
Publisher
» Staff
» Other journals

Bounded saturation-based CTL model checking; pp. 59–70

(Full article in PDF format) doi: 10.3176/proc.2013.1.07


Authors

András Vörös, Dániel Darvas, Tamás Bartha

Abstract

Formal verification is becoming a fundamental step of safety-critical and model-based software development. As part of the verification process, model checking is one of the current advanced techniques to analyse the behaviour of a system. Symbolic model checking is an efficient approach to handling even complex models with huge state spaces. Saturation is a symbolic algorithm with a special iteration strategy, which is efficient for asynchronous models. Recent advances have resulted in many new kinds of saturation-based algorithms for state space generation and bounded state space generation and also for structural model checking. In this paper, we examine how the combination of two advanced model checking algorithms – bounded saturation and saturation-based structural model checking – can be used to verify systems. Our work is the first attempt to combine these approaches, and this way we are able to handle and examine complex or even infinite state systems. Our measurements show that we can exploit the efficiency of saturation in bounded model checking.

Keywords

bounded model checking, saturation, Multiple-valued Decision Diagram, temporal logic, Computation Tree Logic.

References

  1. Biere , A. , Cimatti , A. , Clarke , E. M. , and Zhu , Y. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems , TACAS’99. Springer-Verlag , London , UK , 1999 , 193–207.

  2. Bradley , A. R. SAT-based model checking without unrolling. In VMCAI’11. Springer-Verlag , Berlin , Heidelberg , 2011 , 70–87.

  3. Bruns , G. and Godefroid , P. Model checking partial state spaces with 3-valued temporal logics. In CAV’99. Springer-Verlag , London , UK , 1999 , 274–287.

  4. Buchholz , P. , Ciardo , G. , Donatelli , S. , and Kemper , P. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comput. , 2000 , 12 , 203–222.
http://dx.doi.org/10.1287/ijoc.12.3.203.12634

  5. Ciardo , G. , Lüttgen , G. , and Siminiceanu , R. Saturation: an efficient iteration strategy for symbolic state space generation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS 2031. Springer-Verlag , 2001 , 328–342.
http://dx.doi.org/10.1007/3-540-45319-9_23

  6. Ciardo , G. , Marmorstein , R. , and Siminiceanu , R. The saturation algorithm for symbolic state-space exploration. Int. J. Softw. Tools Technol. Transf. , 2006 , 8(1) , 4–25.
http://dx.doi.org/10.1007/s10009-005-0188-7

  7. Ciardo , G. and Miner , A. S. Storage alternatives for large structured state spaces. In Proceedings of the 9th ICCPE: Modelling Techniques and Tools. Springer-Verlag , London , UK , 1997 , 44–57.

  8. Ciardo , G. and Siminiceanu , R. Structural symbolic CTL model checking of asynchronous systems. In Computer Aided Verification (CAV’03). LNCS 2725. Springer-Verlag , 2003 , 40–53.

  9. Clarke , E. , Grumberg , O. , and Peled , D. A. Model Checking. The MIT Press , 1999.

10. Clarke , E. , McMillan , K. , Campos , S. , and Hartonas-Garmhausen , V. Symbolic model checking. In Computer Aided Verification (Alur , R. and Henzinger , T. , eds). Lecture Notes in Computer Science , Vol. 102. Springer , Berlin , Heidelberg , 1996 , 419–422.
http://dx.doi.org/10.1007/3-540-61474-5_93

11. Heljanko , K. Bounded reachability checking with process semantics. In Proceedings of the 12th International Conference on Concurrency Theory , CONCUR ’01. Springer-Verlag , London , UK , 2001 , 218–232.

12. Kleene , S. Introduction to Metamathematics. Bibliotheca mathematica. Wolters-Noordhoff Pub. , 1971.

13. McMillan , K. L. Interpolation and SAT-based model checking. In CAV , 2003 , 1–13.

14. Ogata , S. , Tsuchiya , T. , and Kikuno , T. SAT-based verification of safe Petri nets. In ATVA’04. LNCS 299. Springer , 2004 , 79–92.

15. Saad , R. , Dal Zilio , S. , and Berthomieu , B. Mixed shared-distributed hash tables approaches for parallel state space construction. In 10th International Symposium on Parallel and Distributed Computing (ISPDC~2011) , Cluj-Napoca , Romania , July 2011. IEEE Computer Society. 2011 , 9–16.

16. Schuele , T. and Schneider , K. Three-valued logic in bounded model checking. In MEMOCODE’05. IEEE Computer Society , Washington , DC , USA , 2005 , 177–186.

17. Skolem , T. A set theory based on a certain 3-valued logic. Mathematica Scandinavica , 1960 , 8 , 127–136.

18. Vörös , A. , Bartha , T. , Darvas , D. , Szabó , T. , Jámbor , A. , and Horváth , Á. Parallel saturation based model checking. In 10th International Symposium on Parallel and Distributed Computing (ISPDC 2011) , Cluj-Napoca , July 2011}. IEEE Computer Society , 2011 , 94–101.

19. Yu , A. , Ciardo , G. , and Lüttgen , G. Decision-diagram-based techniques for bounded reachability checking of asynchronous systems. Int. J. Softw. Tools Technol. Transf. , 2009 , 11 , 117–131.
http://dx.doi.org/10.1007/s10009-009-0099-0

20. Zhao , Y. and Ciardo , G. Symbolic CTL model checking of asynchronous systems using constrained saturation. In ATVA’09. Springer-Verlag , Berlin , Heidelberg , 2009 , 368–381.

 
Back

Current Issue: Vol. 69, Issue 1, 2020




Publishing schedule:
No. 1: 20 March
No. 2: 20 June
No. 3: 20 September
No. 4: 20 December