nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Proof Assisted Symbolic Model Checking for B and Event-B

verfasst von : Sebastian Krings, Michael Leuschel

Erschienen in: Abstract State Machines, Alloy, B, TLA, VDM, and Z

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B. The high-level nature of B and Event-B accounts for complicated constraints arising in these symbolic analysis techniques. In this paper we suggest using static information stemming from proof obligations to simplify occurring constraints. We show how to include proof information in the aforementioned algorithms. Using different benchmarks we compare explicit state to symbolic model checking as well as techniques with and without proof assistance. In particular for models with large branching factor, e.g., due to complicated data values being manipulated, the symbolic techniques fare much better than explicit state model checking. The inclusion of proof information results in further clear performance improvements.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Compact Encoding of Sequential ASMs in Event-B

Nächstes Kapitel On Component-Based Reuse for Event-B

BDD-style model checking [10] is also called symbolic model checking. In recent work ProB has been integrated with LTSMin for such kind of model checking.

In theory, one could export proof information from Atelier B.

ProB gives the user the opportunity to set an upper-bound on the number of successor states per event for the explicit model checker; exhaustive model checking is then not possible but counterexamples can still be found.

We could have added theses constraints \(s_i \ne s_j\) also in Sect. 2.1.

Available at http://stups.hhu.de/ProB. Information on how to use the new algorithms can be found on the ProB wiki: For the BMC\(^*\) algorithm see

http://stups.hhu.de/ProB/Bounded_Model_Checking. The other algorithms are documented at http://stups.hhu.de/ProB/Symbolic_Model_Checking.

For further information regarding TLA\(^+\) support in ProBhave a look at http://stups.hhu.de/ProB/TLA.

Like the Atelier B provers or the SMT solvers for Rodin.

Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRef

Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with event-B. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 178–193. Springer, Heidelberg (2012)CrossRef

Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 21–33. Springer, Heidelberg (2004)CrossRef

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)CrossRef

Biere, A.: Bounded model checking. In: Handbook of Satisfiability, pp. 457–481 (2009)

Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)CrossRef

Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 831–848. Springer, Heidelberg (2014)

Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1–18. Springer, Heidelberg (2014)CrossRef

Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)CrossRef

10.

Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)MathSciNetCrossRefMATH

11.

Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012)CrossRef

12.

Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in Rodin. Sci. Comput. Program. 94(P2), 130–143 (2014)CrossRef

13.

Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD 2011), pp. 125–134, Austin, TX, FMCAD Inc (2011)

14.

Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. Theor. Pract. Logic Program. 11(4–5), 767–782 (2011)MathSciNetCrossRef

15.

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, Heidelberg (2014)CrossRef

16.

Hansen, D., Leuschel, M.: Translating TLA\(^\text{+ }\) 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)CrossRef

17.

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)CrossRef

18.

Krings, S., Bendisposto, J., Leuschel, M.: From failure to proof: the prob disprover for B and event-B. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 199–214. Springer, Heidelberg (2015)CrossRef

19.

Krings, S., Leuschel, M.: SMT Solvers for Validation of B and Event-B models. In: Proceedings iFM’2016, LNCS. Springer (2016). to appear

20.

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)CrossRef

21.

Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRef

22.

Ligot, O., Bendisposto, J., Leuschel, M.: Debugging event-B models using the ProB disprover plug-in. In: Proceedings AFADL 2007, June 2007

23.

Matos, P.J., Fischer, B., Marques-Silva, J.: A lazy unbounded model checker for Event-B. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 485–503. Springer, Heidelberg (2009)CrossRef

24.

Müller, O., Nipkow, T.: Combining model checking and deduction for I/O- automata. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 1–16. Springer, Heidelberg (1995)CrossRef

25.

Plagge, D., Leuschel, M.: Validating B, Z and TLA \(^ \text{+ } \) using ProB and Kodkod. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372–386. Springer, Heidelberg (2012)CrossRef

26.

Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 82. Springer, Heidelberg (2001)CrossRef

27.

Savary, A., Frappier, M., Leuschel, M., Lanet, J.-L.: Model-based robustness testing in event-B using mutation. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 132–147. Springer, Heidelberg (2015)CrossRef

28.

Shankar, N.: Combining theorem proving and model checking through symbolic analysis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 1. Springer, Heidelberg (2000)CrossRef

29.

Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)CrossRef

30.

Witulski, J., Leuschel, M.: Checking computations of formal method tools - a secondary toolchain for prob. In: Proceedings of the 1st Workshop on Formal-IDE (EPTCS), Electronic Proceedings in Theoretical Computer Science, vol. 149 (2014)

31.

Yu, Y., Manolios, P., Lamport, L.: Model checking TLA \(^ \text{+ } \) specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999)CrossRef

Titel: Proof Assisted Symbolic Model Checking for B and Event-B
verfasst von: Sebastian Krings
Michael Leuschel
Verlag: Springer International Publishing
Buch: Abstract State Machines, Alloy, B, TLA, VDM, and Z
Print ISBN: 978-3-319-33599-5

Electronic ISBN: 978-3-319-33600-8

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-33600-8_8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"