nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

01.10.2014 | RERS

BDD-based software verification

Applications to event-condition-action systems

verfasst von: Dirk Beyer, Andreas Stahlbauer

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2014

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

In software model checking, most successful symbolic approaches use predicates as representation of the state space, and SMT solvers for computations on the state space; BDDs are often used as auxiliary data structure. Although BDDs are applied with great success in hardware verification, BDD representations of software state spaces were not yet thoroughly investigated, mainly because not all operations that are needed in software verification are efficiently supported by BDDs. We evaluate the use of a pure BDD representation of integer values, and focus on a particular class of programs: event-condition-action (ECA) programs with limited operations. A symbolic representation using BDDs seems appropriate for ECA programs under certain conditions. We configure a program analysis based on BDDs and experimentally compare it to four approaches to verify reachability properties of ECA programs: an explicit-value analysis, a symbolic bounded-loops analysis, a predicate-abstraction analysis, and a predicate-impact analysis. The results show that BDDs are efficient for a restricted class of programs, which yields the insight that BDDs could be used selectively for variables that are restricted to certain program operations (according to the variable’s domain type), even in general software model checking. We show that even a naive portfolio approach, in which after a pre-analysis either a BDD-based analysis or a predicate-impact analysis is performed, outperforms all above-mentioned analyses.

Vorheriger Artikel Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges

Nächster Artikel Applying symbolic bounded model checking to the 2012 RERS greybox challenge

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

http://rers-challenge.org/.

http://cpachecker.sosy-lab.org/.

https://es-static.fbk.eu/tools/kratos/.

Personal communication with the developers.

The framework CPAchecker [13], which we use to implement the analysis, accepts C programs and transforms them into a side-effect free form [45]; it also supports interprocedural program analysis.

For ease of illustration, we show only a simplified version.

There are Programs 1–19 and 28–54; there is a gap from number 20 to 27, for which no programs exist.

http://www.sosy-lab.org/~dbeyer/cpa-bdd/.

https://svn.sosy-lab.org/software/cpachecker/tags/.

http://javabdd.sourceforge.net/.

Four Eca-Eq programs were removed due to GCC timeout.

Four Eca-Mul programs were removed due to GCC timeout.

Anderson, R.J., Beame, P., Burns, S., Chan, W., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. In: Proc. FSE, pp. 156–166. ACM (1996)

Apel, S., Beyer, D., Friedberger, K., Raimondi, F., Rhein, A.V.: Domain types: Abstract-domain selection based on variable usage. In: Proc. HVC, LNCS 8244, pp. 262–278. Springer, Berlin (2013)

Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstractions for model checking C programs. In: Proc. TACAS, LNCS 2031, pp. 268–283. Springer, Berlin (2001)

Berndl, M., Lhoták, O., Qian, F., Hendren, L., Umanee, N.: Points-to analysis using BDDs. In: Proc. PLDI, pp. 103–114. ACM (2003)

Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Proc. FME, LNCS 2021, pp. 318–343. Springer, Berlin (2001)

Beyer, D.: Relational programming with CrocoPat. In: Proc. ICSE, pp. 807–810. ACM (2006)

Beyer, D.: Second competition on software verification. In: Proc. TACAS, LNCS 7795, pp. 594–609. Springer, Berlin (2013)

Beyer, D.: Status report on software verification. In: Proc. TACAS, LNCS 8413, pp. 373–388. Springer, Berlin (2014)

Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proc. FMCAD, pp. 25–32. IEEE (2009)

10.

Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5–6), 505–525 (2007)CrossRef

11.

Beyer, D., Henzinger, T. A., Théoduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Proc. CAV, LNCS 4590, pp. 504–518. Springer, Berlin (2007)

12.

Beyer, D., Henzinger, T. A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE, pp. 29–38. IEEE (2008)

13.

Beyer, D., Keremoglu, M. E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV, LNCS 6806, pp. 184–190. Springer, Berlin (2011)

14.

Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD, pp. 189–197. FMCAD (2010)

15.

Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A tool for BDD-based verification of real-time systems. In: Proc. CAV, LNCS 2725, pp. 122–125. Springer, Berlin (2003)

16.

Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proc. FASE, LNCS 7793, pp. 146–162. Springer, Berlin (2013)

17.

Beyer, D., Noack, A.: Can decision diagrams overcome state space explosion in real-time verification? In: Proc. FORTE, LNCS 2767, pp. 193–208. Springer, Berlin (2003)

18.

Beyer, D., Stahlbauer, A.: BDD-based software model checking with CPAchecker. In: Proc. MEMICS, LNCS 7721, pp. 1–11. Springer, Berlin (2013)

19.

Beyer, D., Wendler, P.: Algorithms for software model checking: Predicate abstraction vs. Impact. In: Proc. FMCAD, pp. 106–113. FMCAD (2012)

20.

Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS, LNCS 1579, pp. 193–207. Springer, Berlin (1999)

21.

Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and symbolic reachability. In: Proc. CAV, LNCS 6174, pp. 354–359. Springer, Berlin (2010)

22.

Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)CrossRefMATH

23.

Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine. S.: Kronos: A model-checking tool for real-time systems. In: Proc. CAV, LNCS 1427, pp. 546–550. Springer, Berlin (1998)

24.

Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8):677–691 (1986)

25.

Bryant, R.E.: On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205–213 (1991)CrossRefMATHMathSciNet

26.

Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: Proc. DAC, pp. 46–51. ACM (1990)

27.

Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. In: Proc. LICS, pp. 428–439. IEEE (1990)

28.

Campos, S.V.A., Clarke, E.M.: The Verus language: representing time efficiently with BDDs. In: Proc. ARTS, LNCS 1231, pp. 64–78. Springer, Berlin (1997)

29.

Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An open-source tool for symbolic model checking. In: Proc. CAV, LNCS 2404, pp. 359–364. Springer, Berlin (2002)

30.

Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Proc. CAV, LNCS 1633, pp. 495–499. Springer, Berlin (1999)

31.

Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos: A software model checker for SystemC. In: Proc. CAV, LNCS 6806, pp. 310–316. Springer, Berlin (2011)

32.

Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proc. TACAS, LNCS 7795, pp. 93–107. Springer, Berlin (2013)

33.

Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)CrossRefMathSciNet

34.

Craig, W.: Linear reasoning. A new form of the Herbrand–Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)CrossRefMATHMathSciNet

35.

Esparza, J.: Building a software model checker. In: Proc. Formal logical methods for system security and correctness, pp. 53–87. IOS Press (2008)

36.

Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: Proc. TACAS, LNCS 3920, pp. 489–503. Springer, Berlin (2006)

37.

Henzinger, T. A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL, pp. 232–244. ACM (2004)

38.

Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58–70. ACM (2002)

39.

Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: Analysis of event–condition–action systems. In: Proc. ISoLA, LNCS 7609, pp. 608–614. Springer, Berlin (2012)

40.

Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Păsăreanu, C.S.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. Int. J. Softw. Tools Technol. Transfer. doi:10.1007/s10009-014-0337-y (2014)

41.

Ivanc̆ić, F., Shlyakhter, I., Gupta, A., Ganai, M.K., Kahlon, V., Wang, C., Yang, Z.: Model checking C programs using F-Soft. In: Proc. ICCD, pp. 297–308. IEEE (2005)

42.

Lerda, F., Sinha, N., Theobald, M.: Symbolic model checking of software. Electr. Notes Theor. Comput. Sci. 89(3), 480–498 (2003)CrossRef

43.

McMillan, K.L.: The SMV system. Technical Report CMU-CS-92-131. Carnegie Mellon University (1992)

44.

McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. CAV, LNCS 4144, pp. 123–136. Springer, Berlin (2006)

45.

Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of C programs. In: Proc. CC, LNCS 2304, pp. 213–228. Springer, Berlin (2002)

46.

Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation. In: Proc. SPIN, LNCS 7976, pp. 341–357. Springer, Berlin (2013)

47.

Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: Synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transfer. doi:10.1007/s10009-014-0336-z (2014)

48.

von Rhein, A., Apel, S., Raimondi, F.: Introducing binary decision diagrams in the explicit-state verification of Java code. In: Proceedings of Java Pathfinder Workshop (2011)

Titel: BDD-based software verification
Applications to event-condition-action systems
verfasst von: Dirk Beyer
Andreas Stahlbauer
Publikationsdatum: 01.10.2014
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 5/2014
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-014-0334-1

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"

Weitere Artikel der Ausgabe 5/2014

A multiple case study on risk-based testing in industry

Risk-based testing via active continuous quality control

Approaches for the combined use of risk analysis and testing: a systematic literature review

A taxonomy of risk-based testing

Tailored generation of concurrent benchmarks

Rigorous examination of reactive systems

Premium Partner