Skip to main content
SpringerLink
Log in

Bounded Model Checking High Level Petri Nets in PIPE+Verifier

  • Conference paper
Book cover Formal Methods and Software Engineering (ICFEM 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8829))

Included in the following conference series:

Abstract

High level Petri nets (HLPNs) have been widely applied to model concurrent and distributed systems in computer science and many other engineering disciplines. However, due to the expressive power of HLPNs, they are more difficult to analyze. Exhaustive analysis methods such as traditional model checking based on fixed point calculation of state space may not work for HLPNs due to the state explosion problem. Bounded model checking (BMC) using satisfiability solvers is a promising analysis method that can handle a much larger state space than traditional model checking method. In this paper, we present an analysis method for HLPNs by leveraging the BMC technique with a state-of-the-art satisfiability modulo theories (SMT) solver Z3. A HLPN model and some safety properties are translated into a first order logic formula that is checked by Z3. This analysis method has been implemented in a tool called PIPE+Verifier and is completely automatic. We show our results of applying PIPE+Verifier to several models from the Model Checking Contest @ Petri Nets and a few other sources.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. CPN tools, http://cpntools.org

  2. High-level Petri Nets - Concepts, Definitions and Graphical Notation (2000)

    Google Scholar 

  3. Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using smt solvers instead of sat solvers. Int. J. Softw. Tools Technol. Transf. 11(1), 69–83 (2009)

    Article  Google Scholar 

  4. Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation 183(2), 140–164 (2003); 12th International Conference on Rewriting Techniques and Applications (RTA 2001)

    Google Scholar 

  5. Ball, T., Bounimova, E., Kumar, R., Levin, V.: Slam2: static driver verification with under 4. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Austin, TX, pp. 35–42. FMCAD Inc. (2010)

    Google Scholar 

  6. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Barrett, C., De Moura, L., Stump, A.: Design and results of the 1st satisfiability modulo theories competition (smt-comp.). Journal of Automated Reasoning 35, 2005 (2005)

    Google Scholar 

  8. Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010), http://www.SMT-LIB.org

  9. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Chiola, G., Franceschinis, G.: Colored gspn models and automatic symmetry detection. In: PNPM, pp. 50–60 (1989)

    Google Scholar 

  12. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  13. Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. In: Formal Methods in System Design, p. 2001. Kluwer Academic Publishers (2001)

    Google Scholar 

  14. Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. Clarke, E., Kroning, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85–96. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)

    Article  Google Scholar 

  17. De Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)

    Article  MATH  Google Scholar 

  19. Dutertre, B., De Moura, L.: The yices smt solver 2, 2 (2006), Tool paper, http://yices.csl.sri.com/tool-paper.pdf

  20. Allen Emerson, E., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275–306 (1987)

    Article  MATH  Google Scholar 

  21. Fronc, Ł., Duret-Lutz, A.: LTL model checking with neco. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 451–454. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  22. Holzmann, G.: Spin model checker, the: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)

    Google Scholar 

  23. Hostettler, S., Marechal, A., Linard, A., Risoldi, M., Buchs, D.: High-level petri net model checking with alpina. Fundam. Inf. 113(3-4), 229–264 (2011)

    MathSciNet  MATH  Google Scholar 

  24. Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)

    Google Scholar 

  25. Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and cpn tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3), 213–254 (2007)

    Article  Google Scholar 

  26. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (1999)

    Google Scholar 

  27. Kordon, F., Linard, A., Becutti, M., Buchs, D., Fronc, L., Hulin-Hubard, F., Legond-Aubry, F., Lohmann, N., Marechal, A., Paviot-Adet, E., Pommereau, F., Rodrígues, C., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Web report on the model checking contest @ petri net 2013 (June 2013), http://mcc.lip6.fr

  28. Kordon, F., Linard, A., Beccuti, M., Buchs, D., Fronc, L., Hillah, L.-M., Hulin-Hubard, F., Legond-Aubry, F., Lohmann, N., Marechal, A., Paviot-Adet, E., Pommereau, F., Rodríguez, C., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Model checking contest @ petri nets, report on the 2013 edition. CoRR, abs/1309.2485 (2013)

    Google Scholar 

  29. Kröning, D., Rümmer, P., Weissenbacher, G.: A proposal for a theory of finite sets, lists, and maps for the smt-lib standard. In: Informal proceedings, 7th International Workshop on Satisfiability Modulo Theories at CADE 22 (2009)

    Google Scholar 

  30. Liu, S., Zeng, R., He, X.: Pipe+ - a modeling tool for high level petri nets. In: SEKE, pp. 115–121 (2011)

    Google Scholar 

  31. Liu, S., Zeng, R., Sun, Z., He, X.: Samat - a tool for software architecture modeling and analysis. In: SEKE, pp. 352–358 (2012)

    Google Scholar 

  32. de Moura, L., Bjørner, N.: Satisfiability Modulo Theories: An Appetizer. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol. 5902, pp. 23–36. Springer, Heidelberg (2009)

    Google Scholar 

  33. Srivastava, S., Gulwani, S., Foster, J.S.: VS3: SMT Solvers for Program Verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 702–708. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  34. Stepney, S.: An Electronic Purse: Specification, Refinement, and Proof. Technical monograph. Oxford University Computing Laboratory, Programming Research Group (2000)

    Google Scholar 

  35. Stump, A., Barrett, C.W., Dill, D.L.: A decision procedure for an extensional theory of arrays. In: 16th IEEE Symposium on Logic in Computer Science, pp. 29–37. IEEE Computer Society (2001)

    Google Scholar 

  36. Ullman, J.D.: Elements of ML programming (ML97 ed.). Prentice-Hall, Inc., Upper Saddle River (1998)

    Google Scholar 

  37. Veanes, M., Bjørner, N., Gurevich, Y., Schulte, W.: Symbolic bounded model checking of abstract state machines. Int. J. Software and Informatics 3(2-3), 149–170 (2009)

    Google Scholar 

  38. Veanes, M., Bjørner, N.S., Raschke, A.: An SMT approach to bounded reachability analysis of model programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 53–68. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  39. Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engg. 10(2), 203–232 (2003)

    Article  Google Scholar 

  40. Woodcock, J.: First steps in the verified software grand challenge. Computer 39(10), 57–64 (2006)

    Article  Google Scholar 

  41. Woodcock, J., Stepney, S., Cooper, D., Clark, J.A., Jacob, J.: The certification of the mondex electronic purse to itsec level e6. Formal Asp. Comput. 20(1), 5–19 (2008)

    Article  Google Scholar 

  42. Zeng, R., He, X.: Analyzing a formal specification of mondex using model checking. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 214–229. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  43. Zeng, R., Liu, J., He, X.: A formal specification of mondex using sam. In: IEEE International Symposium on Service-Oriented System Engineering, SOSE 2008, pp. 97–102 (December 2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Florida International University, Miami, Florida, 33199, USA

    Su Liu, Reng Zeng, Zhuo Sun & Xudong He

Authors
  1. Su Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Reng Zeng
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zhuo Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Xudong He
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Inria Nancy - Grand Est, 615 rue du Jardin Botanique, 54602, Villers-lès-Nancy, France

    Stephan Merz

  2. Université du Luxembourg, 6 rue Richard Coudenhove-Kalergi, 1359, Luxembourg, Luxembourg

    Jun Pang

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Liu, S., Zeng, R., Sun, Z., He, X. (2014). Bounded Model Checking High Level Petri Nets in PIPE+Verifier. In: Merz, S., Pang, J. (eds) Formal Methods and Software Engineering. ICFEM 2014. Lecture Notes in Computer Science, vol 8829. Springer, Cham. https://doi.org/10.1007/978-3-319-11737-9_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11737-9_23

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11736-2

  • Online ISBN: 978-3-319-11737-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation