Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 4/2013

01.08.2013 | TACAS 2009

Selected dynamic issues in software model checking

verfasst von: Viet Yen Nguyen, Theo C. Ruys

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 4/2013

Einloggen

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

search-config
loading …

Abstract

Software model checking has come of age. After one and a half decade, several successful model checking tools have emerged. One of the most prominent approaches is the virtual machine-based approach, pioneered by Java PathFinder (jpf). And although the virtual machine-based approach has been rather successful, it lags behind classic model checking in terms of speed and memory consumption. Fortunately, with respect to the implementation of virtual-based model checkers, there is still ample room for innovation and optimizations. This paper presents three novel (optimization) techniques that have been implemented into MoonWalker, a software model checker for .Net programs. (a) .Net specifies an exception handling mechanism called structured exception handling (seh). seh is one of the most sophisticated and fine-grained exception handling mechanisms for application platforms. Its implementation within MoonWalker is the most sophisticated in a model checker to date. (b) To decrease memory use within MoonWalker, a collapsing scheme has been developed for collapsing the metadata used by stateful dynamic partial order reduction. The reduction of memory is—in some cases—more than a factor of two. (c) Finally, to decrease the verification time, the memoised garbage collection (mgc) algorithm has been developed. It has a lower time-complexity than the often used Mark & Sweep garbage collector. Its main idea is that it only traverses changed parts of the heap instead of the full heap. The average time reduction is up to 25%. We have used the Java Grande Forum benchmark suite to compare MoonWalker against jpf and observed that the average performance of MoonWalker is on par with jpf.
Vorheriger Artikel Static analysis for concurrent programs with applications to data race detection
Nächster Artikel A model-driven co-simulation environment for heterogeneous systems

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
Fußnoten
1
Moon is an anagram of Mono. Walker refers to the nature of the tool: walking the state space of cil bytecode programs. MoonWalker was previously known as mmc: the Mono Model Checker. Due to several name clashes—e.g. the Mobility Model Checker for the pi-calculus [44], Microsoft’s Management Console, the Mickey Mouse Club—the name has been changed to MoonWalker.
 
Literatur
1.
Aan de Brugh, N.H.M., Nguyen, V.Y., Ruys, T.: MoonWalker: verification of.NET programs. In : Kowalewski, S., Philippou, A. (eds.). Proceedings of the 15th International Conference on TACAS 2009, York, UK, March, 2009, LNCS, vol. 5505, pp. 170–173. Springer, Berlin (2009)
2.
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: a model checker for concurrent software. In: Alur, R., Peled, D. (eds.) Proceedings of 16th International Conference on Computer Aided Verification (CAV 2004), Boston, MA, USA, LNCS, vol. 3114, pp. 484–487. Springer, Berlin (2004)
3.
Arnold, K., Gosling, J., Holmes, D.: Java Language Specification. Prentice Hall, Englewood Cliffs (2005)
4.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, New York (2008)MATH
5.
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th Symposium on Principles of Programming Languages (POPL 2002), pp. 1–3 (2002)
6.
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast: applications to software engineering. Softw. Tools Technol. Transf. (STTT) 9(5-6), 505–525 (2007)CrossRef
7.
Cherkassky, B.V., Goldberg, A.V., Silverstein, C.: Buckets, heaps, lists, and monotone priority queues. In: Saks, M. (ed.) Proceedings of the 8th ACM-SIAM Symposium on Discrete Algorithms (SODA’97), New Orleans, LA, USA. Society for Industrial and Applied Mathematics, pp. 83–92 (1997)
8.
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Proceedings of the 10th International Conference on TACAS 2004, Barcelona, ES. LNCS, vol. 2988, pp. 168–176. Springer, Berlin (2004)
9.
Clarke, E.M., Emerson, E.A. Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Proceedings of the 10th International Conference on Computer Aided Verification (CAV 1998), LNCS, vol. 1427, pp. 147–158. Springer, Berlin (1998)
10.
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
11.
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: Proceedings of 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, pp. 439–448. ACM, New York (2000)
12.
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: Bandera: a source-level interface for model checking Java programs. In: Proceedings of 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, pp. 762–765. ACM, New Yorl (2000)
13.
14.
Dwyer, M.B., Hatcliff, J.: Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. Formal Methods Syst Des 25(2–3), 199–240 (2004)
15.
16.
Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: efficiently computing the happens-before relation using locksets. In: Havelund, K., Núñez, M., Rosu, G., Wolff, B. (eds.) Proceedings of First Combined International Workshops on Formal Approaches to Software Testing (FATES 2006) and Runtime Verification (RV 2006), Seattle, WA, USA, LNCS 4262, pp. 193–208. Springer, Berlin (2006)
17.
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Palsberg, J., Abadi, M. (eds.) Proceedings of POPL 2005, pp. 110–121. ACM, New York (2005)
18.
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Boston (1995)
19.
Godefroid, P.: Partial-order methods for the verification of concurrent systems—an Approach to the state-explosion problem. PhD in Computer Science, University of Liege, Nov. 1994. (A revised version has been published as LNCS 1032, Springer (1996))
20.
Grieskamp, W., Tillmann, N., Schulte, W.: XRT: exploring runtime for.NET—architecture and applications. Electr. Notes Theor. Comput. Sci. (ENTCS) 144(3), 3–26 (2006)CrossRef
21.
Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Softw. Tools Technol. Transfer (STTT) 2(4), 366–381 (2000)MATHCrossRef
22.
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) Proceedings of the 10th International SPIN Workshop (SPIN 2003), Portland, OR, USA, May 9–10, LNCS, vol. 2648, pp. 235–239. Springer, Berlin (2003)
23.
Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proceedings of the 3th International SPIN Workshop (SPIN 1997), University of Twente, Enschede, The Netherlands (1997)
24.
Holzmann, G.J.: The SPIN Model Checker—Primer and Reference Manual. Addison-Wesley, Boston (2004)
25.
Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) Proceedings of the 15th International SPIN Workshop (SPIN 2008), Los Angeles, CA, USA, August, LNCS, vol. 5126, pp. 134–143. Springer, Berlin (2008)
26.
Holzmann, G.J., Smith, M.H.: Software model checking. In: Wu, J., Chanson, S.T., Gao, Q (eds.) Proceedings of FORTE/PSTV 1999, IFIP Conference Proceedings, vol. 156, pp. 481–497. Kluwer, Hingham (1999)
27.
Iosif, R.: Exploiting heap symmetries in explicit-state model checking of software. In: Proceedings of the 16th International Conference on Automated Software Engineer (ASE 2001), San Diego, USA, November, pp. 254–261. IEEE Computer Society (2001)
28.
Iosif, R.: Symmetry reductions for model checking of concurrent dynamic software. Softw. Tools Technol. Transf. (STTT) 6(4), 302–319 (2004)MathSciNetCrossRef
29.
Iosif, R., Sisto, R.: Using garbage collection in model checking. In: Havelund, K., Penix, J., Visser, W. (eds.) Proceedings of the 7th International SPIN Workshop (SPIN 2000), Stanford, CA, USA, LNCS, vol. 1885, pp. 20–33. Springer, Berlin (2000)
30.
Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M.B., (ed.) Proceedings of the 8th International SPIN Workshop (SPIN 2001), Toronto, Canada, LNCS, vol. 2057, pp. 80–102. Springer, Berlin (2001)
31.
Lidin, S.: Inside Microsoft.NET IL Assembler. Microsoft Press, USA (2002)
32.
McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3(4), 184–195 (1960)MATHCrossRef
33.
Musuvathi, M., Dill, D.L.: An incremental heap canonicalization algorithm. In: Godefroid, P. (ed.) Proceedings of the 12th International SPIN Workshop (SPIN 2005), San Francisco, CA, USA, LNCS, vol. 3639, pp. 28–42. Springer, Berlin (2005)
34.
Nguyen, V.Y.: Optimising techniques for model checkers. Master’s thesis, University of Twente, Enschede (2007)
35.
Nguyen V.Y., Ruys, T.C.: Memoised garbage collection for software model checking. In: Kowalewski S., Philippou A., (eds.) Proceedings of the 15th International Conference on TACAS 2009, York, UK, LNCS, vol. 5505, pp. 201–214. Springer, Berlin (2009)
36.
Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) Proceedings of the 11th International Conference on TACAS 2005, Edinburgh, UK, LNCS, vol. 3440, pp. 93–107. Springer, Berlin (2005)
37.
Ramalingam, G., Reps, T.W.: An incremental algorithm for a generalization of the shortest-path problem. J. Algorithm. 21(2), 267–305 (1996)MathSciNetMATHCrossRef
38.
Ranganath, V.P., Hatcliff, J., Robby: Enabling efficient partial order reductions for model checking object-oriented programs using static calculation of program dependencies. Technical Report SAnToS-TR2007-2, SAnToS Laboratory, CIS Department, Kansas State University (2007)
39.
Robby, Dwyer, M.B., Hatcliff, J.: BOGOR: an extensible and highly-modular software model checking framework. In: Proceedings of ESEC/SIGSOFT FSE, New York, NY, USA, pp. 267–276, ACM Press, New York (2003)
40.
Ruys, T.C., Aan de Brugh, N.H.M.: MMC: the mono model checker. ENTCS, 190(1):149–160 (2007). (Proceedings of Bytecode, Braga, Portugal (2007))
41.
Smith, L.A., Bull, J.M., Obdrzálek, J.: A parallel Java grande benchmark suite. In: Proceedings of the 2001 ACM/IEEE Conference on Supercomputing (SC 2001), pp. 8–8. ACM, New York (2001)
42.
Tillmann, N., Halleux, J.D.: PEX: White box test generation for .NET. In: Beckert, B., Haehnle, R. (eds.) Proceedings of the 2nd International Conference on TAP 2008, Prato, IT, LNCS, vol. 4966, pp. 134–153. Springer, Berlin (2008)
43.
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. (ASE) 10(2), 203–232 (2003)CrossRef
44.
Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A logical encoding of the \(\pi \)-calculus: model checking mobile processes using tabled resolution. Softw. Tools Technol. Transf. (STTT) 6(1), 38–66 (2004)
45.
Yi, X., Wang, J., Yang, X.: Stateful dynamic partial-order reduction. In: Liu, Z., He, J. (eds.) Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM 2006), LNCS, vol. 4260, pp. 149–167. Springer, Berlin (2006)
46.
47.
48.
49.
50.
51.
52.
53.
Metadaten
Titel
Selected dynamic issues in software model checking
verfasst von
Viet Yen Nguyen
Theo C. Ruys
Publikationsdatum
01.08.2013
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 4/2013
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-012-0261-y

Weitere Artikel der Ausgabe 4/2013

International Journal on Software Tools for Technology Transfer 4/2013 Zur Ausgabe

Introduction

Model checking and abstract interpretation as building blocks of advanced program analysis techniques

Regular Paper

A model-driven co-simulation environment for heterogeneous systems

TACAS 2009

From tests to proofs

Regular Paper

An integrated framework for checking the behaviour of fUML models using CSP

TACAS 2009

Falsification of LTL safety properties in hybrid systems

TACAS 2009

Static analysis for concurrent programs with applications to data race detection