Skip to main content
SpringerLink
Log in
Book cover

NASA Formal Methods Symposium

NFM 2018: NASA Formal Methods pp 244–260Cite as

Distributed Model Checking Using ProB

  • Conference paper
  • First Online:

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

Abstract

Model checking larger specifications can take a lot of time, from several minutes up to weeks. Naturally, this renders the development of a correct specification very cumbersome. If the model offers enough non-determinism, however, we can distribute the workload onto multiple computers in order to reduce the runtime.

In this paper, we present distb, a distributed version of ProB’s model checker. Furthermore, we show possible speed-ups for real-life formal models on both a single workstation and a high-performance cluster.

This is a preview of subscription content, 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 EPUB and 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

Learn about institutional subscriptions

Notes

  1. 1.

    Strictly spoken, it should be a 27-ary trie including an end-of-word symbol in order to store both a word and one of its prefixes. Since the data we store has a fixed length, we omit this detail.

References

  1. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)

    Book  MATH  Google Scholar 

  2. Abrial, J.-R., Lee, M.K.O., Neilson, D.S., Scharbach, P.N., Sørensen, I.H.: The B-method. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 398–405. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0020001

    Chapter  Google Scholar 

  3. Bagwell, P.: Ideal Hash Trees. Es Grands Champs, vol. 1195 (2001)

    Google Scholar 

  4. Bendisposto, J., Körner, P., Leuschel, M., Meijer, J., van de Pol, J., Treharne, H., Whitefield, J.: Symbolic reachability analysis of B through ProB and LTSmin. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 275–291. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_18

    Chapter  Google Scholar 

  5. Bendisposto, J., Leuschel, M.: Proof assisted model checking for B. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 504–520. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10373-5_26

    Chapter  Google Scholar 

  6. Bendisposto, J.M.: Directed and distributed model checking of B-specifications. Ph.D. thesis, Universitäts- und Landesbibliothek der Heinrich-Heine-Universität Düsseldorf (2015)

    Google Scholar 

  7. Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_31

    Chapter  Google Scholar 

  8. Carlsson, M., Widen, J., Andersson, J., Andersson, S., Boortz, K., Nilsson, H., Sjöland, T.: SICStus Prolog User’s Manual, vol. 3. Swedish Institute of Computer Science Kista, Sweden (1988)

    Google Scholar 

  9. DEPLOY Deliverable: D20-Report on Pilot Deployment in the Space Sector. FP7 ICT DEPLOY Project, January 2010. http://www.deploy-project.eu/html/deliverables.html

  10. Ghemawat, S., Dean, J.: LevelDB (2011). https://github.com/google/leveldb

  11. Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 66–79. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07512-9_5

    Chapter  Google Scholar 

  12. Hansen, D., Leuschel, M.: Translating TLA\(^{+}\) to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24–38. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30729-4_3

    Chapter  Google Scholar 

  13. Hansen, D., Leuschel, M.: Translating B to TLA\(^{+}\) for validation with TLC. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 40–55. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_4

    Chapter  Google Scholar 

  14. Hintjens, P.: ZeroMQ: Messaging for Many Applications. O’Reilly Media Inc., Newton (2013)

    Google Scholar 

  15. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  16. Knuth, D.E.: The Art of Computer Programming: Sorting and Searching, vol. III. Addison-Wesley, Boston (1973)

    MATH  Google Scholar 

  17. Körner, P.: Improving distributed model checking in ProB. Bachelor’s thesis, Heinrich Heine Universität Düsseldorf, August 2014

    Google Scholar 

  18. Körner, P.: An integration of ProB and LTSmin. Master’s thesis, Heinrich Heine Universität Düsseldorf, February 2017

    Google Scholar 

  19. Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48234-2_3

    Chapter  Google Scholar 

  20. Leuschel, M.: The high road to formal validation: model checking high-level versus low-level specifications. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 4–23. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87603-8_2

    Chapter  Google Scholar 

  21. Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46

    Chapter  Google Scholar 

  22. Prokopec, A., Bagwell, P., Odersky, M.: Cache-aware lock-free concurrent hash tries. arXiv preprint arXiv:1709.06056 (2017)

  23. Sayrafiezadeh, M.: The birthday problem revisited. Math. Mag. 67(3), 220–223 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  24. Venkatramani, C., Chiueh, T.-C.: Design, implementation, and evaluation of a software-based real-time ethernet protocol. ACM SIGCOMM Comput. Commun. Rev. 25(4), 27–37 (1995)

    Article  Google Scholar 

  25. Yeo, C.K., Lee, B.-S., Er, M.: A survey of application level multicast techniques. Comput. Commun. 27(15), 1547–1568 (2004)

    Article  Google Scholar 

  26. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA\(^{+}\) specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48153-2_6

    Chapter  Google Scholar 

Download references

Acknowledgement

Computational support and infrastructure was provided by the “Centre for Information and Media Technology” (ZIM) at the University of Düsseldorf (Germany).

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Düsseldorf, Universitätsstr. 1, 40225, Düsseldorf, Germany

    Philipp Körner & Jens Bendisposto

Authors
  1. Philipp Körner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jens Bendisposto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Philipp Körner .

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, Hampton, Virginia, USA

    Aaron Dutle

  2. NASA Langley Research Center, Hampton, Virginia, USA

    César Muñoz

  3. NASA Langley Research Center, Hampton, Virginia, USA

    Anthony Narkawicz

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Körner, P., Bendisposto, J. (2018). Distributed Model Checking Using ProB . In: Dutle, A., Muñoz, C., Narkawicz, A. (eds) NASA Formal Methods. NFM 2018. Lecture Notes in Computer Science(), vol 10811. Springer, Cham. https://doi.org/10.1007/978-3-319-77935-5_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-77935-5_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-77934-8

  • Online ISBN: 978-3-319-77935-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation