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
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 4/2012

01.10.2012 | Expert’s Voice

The hidden models of model checking

verfasst von: Willem Visser, Matthew B. Dwyer, Michael Whalen

Erschienen in: Software and Systems Modeling | Ausgabe 4/2012

Einloggen

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

search-config
loading …

Abstract

In the past, applying formal analysis, such as model checking, to industrial problems required a team of formal methods experts and a great deal of effort. Model checking has become popular, because model checkers have evolved to allow domain-experts, who lack model checking expertise, to analyze their systems. What made this shift possible and what roles did models play in this? That is the main question we consider here. We survey approaches that transform domain-specific input models into alternative forms that are invisible to the user and which are amenable to model checking using existing techniques—we refer to these as hidden models. We observe that keeping these models hidden from the user is in fact paramount to the success of the domain-specific model checker. We illustrate the value of hidden models by surveying successful examples of their use in different areas of model checking (hardware and software) and how a lack of suitable models hamper a new area (biological systems).
Vorheriger Artikel Lessons learned from building model-driven development tools
Nächster Artikel What makes a good process model?

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 "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

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
Fußnoten
1
When discussing applications of model checking the use of the word “model” has lead to some confusion. Typically the transition system that is provided to a model checker represents an abstract model that captures, e.g., a hardware design description or a software implementation. In this context it makes sense to “check” the “model” to detect errors and this is precisely what that application of model checking does. The word “model” in model checking refers, however, to the fact that model checking determines whether the system is a “logical model” of the property specification, i.e., whether the system satisfies the property.
 
Literatur
1.
2.
3.
Amla, N., Emerson, A.E., Namjoshi, K.S., Trefler, R.J.: Abstract patterns of compositional reasoning. In: CONCUR, pp. 423–438 (2003)
4.
Ball, T., Rajamani, S.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of CAV, Paris, France. LNCS, vol. 2102, pp. 260–264. Springer, Berlin (2001)
5.
Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Proceedings of the 7th International SPIN Workshop on Model Checking and Software Verification, pp. 113–130 (2000)
6.
Batt, G., Belta, C., Weiss, R.: Model checking liveness properties of genetic regulatory networks. In: Tools and Algorithms for the Construction and Analysis of Systems, vol. 4424, pp. 323–338. Springer, Berlin (2007)
7.
Batt, G., Page, M., Cantone, I., Goessler, G., Monteiro, P.T., de Jong, H.: Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18) (2010)
8.
Baumgartner, J., Heyman, T., Singhal, V., Aziz, A.: Model checking the IBM gigahertz processor: an abstraction algorithm for high-performance netlists. In: Proceedings of the 11th International Conference on Computer Aided Verification, pp. 72–83 (1999)
9.
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Formal Methods Syst. Des. 18, 141–163 (2001)MATHCrossRef
10.
Berthomieu, B., Garavel, H., Lang, F., Vernadat, F.: Verifying dynamic properties of industrial critical systems using TOPCASED/FIACRE. ERCIM News 2008(75) (2008)
11.
Bjesse, P., Boralv, A.: Dag-aware circuit compression for formal verification. In: Proceedings of ICCAD ’04, pp. 42–49 (2004)
12.
Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: Proceedings of the 27th Design Automation Conference, pp. 40–45 (1990)
13.
Brand, D.: Verification of large synthesized designs. Proc. ICCAD 1993, 534–537 (1993)
14.
Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI’08, Berkeley, CA, USA, pp. 209–224. USENIX Association (2008)
15.
Cadar, C., Godefroid, P., Khurshid, S., Pǎsǎreanu, C.S., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice: preliminary assessment. In: ICSE, pp. 1066–1071 (2011)
16.
Calder, M., Gilmore, S., Hillston, J., Vyshemirsky, V.: Formal methods for biochemical signalling pathways. In: Formal Methods: State of the Art and New Directions, pp. 185–215. Springer, Berlin (2010)
17.
Chan, W., Anderson, R.J., Beame, P., Jones, D.H., Notkin, D., Warner, W.E.: Optimizing symbolic model checking for statecharts. IEEE Trans. Softw. Eng. 27(2), 170–190 (2001)CrossRef
18.
Chan, W., Anderson, R.J., Beame, P., Notkin, D.: Improving efficiency of symbolic model checking for state-based system requirements. In: ISSTA, pp. 102–112 (1998)
19.
Choi, Y., Rayadurgam, S., Heimdahl, M.P.E.: Toward automation for model-checking requirements specifications with numeric constraints. Requir. Eng. 7(4), 225–242 (2002)CrossRef
20.
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: an open source tool for symbolic model checking. In: Proceedings of the International Conference on Computer-Aided Verification (CAV 2002). Springer, Berlin (2002)
21.
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). Lecture Notes in Computer Science, vol. 2988, pp. 168–176. Springer, Berlin (2004)
22.
Clarke, E.M., Emerson, A.E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Workshop on Logics of Programs, pp. 52–71 (1981)
23.
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV, pp. 154–169 (2000)
24.
Clarke, E.M.: Grumberg. Model Checking. MIT Press, Orna (1999)
25.
Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation, pp. 85–96 (2004)
26.
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Zheng, R., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: International Conference on Software Engineering, pp. 439–448 (2000)
27.
Darringer, A., Joyner, W.H. Jr., Berman, C.L., Trevillyan, L.: Logic synthesis through local transformations. IBM J. Res. Dev. 25(4), 272–280 (1981)
28.
de Halleux, J., Tillmann, N.: Moles: tool-assisted environment isolation with closures. In: Objects, Models, Components, Patterns, pp. 253–270. Springer, Berlin (2010)
29.
Deng, X., Lee, J., Robby: Bogor/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: ASE (2006)
30.
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the International Conference on Software Engineering, pp. 411–420 (1999)
31.
32.
Dwyer, M.B., Hatcliff, J., Robby, Ranganath, V.P.: 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)
33.
Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Berlin (2006)
34.
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Computer Aided Verification, pp. 232–247 (2000)
35.
Fisher, J., Henzinger, T., Mateescu, M., Piterman, N.: Bounded asynchrony: concurrency for modeling cell–cell interactions. In: Formal Methods in Systems Biology, pp. 17–32. Springer, Berlin (2008)
36.
Fisher, J., Henzinger, T.A.: Executable cell biology. Nat. Biotechnol. 25(11), 1239–1249 (2007)CrossRef
37.
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’05, pp. 110–121. ACM, New York (2005)
38.
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D., (eds.) Proceedings of the 16th International Conference on Computer Aided Verification, CAV’04 (Boston, Massachusetts). Lecture Notes in Computer Science, vol. 3114, pp. 175–188. Springer, Berlin (2004)
39.
Giannakopoulou, D., Pǎsǎreanu, C.S., Cobleigh, J.M.: Assume-guarantee verification of source code with design-level assumptions. In: Proceedings of the 26th International Conference on Software Engineering, pp. 211–220 (2004)
40.
Godefroid, P.: Model checking for programming languages using Verisoft. In: Proceedings of POPL, pp. 174–186. ACM, New York (1997)
41.
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems—An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032. Springer, Berlin (1996)
42.
Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. SIGPLAN Not. 40(6), 213–223 (2005)CrossRef
43.
Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network Distributed Security Symposium (NDSS). Internet Society (2008)
44.
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254, pp. 72–83. Springer, Berlin (1997)
45.
Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with Explain. In: CAV, pp. 453–456 (2004)
46.
Groce, A., Visser, W.: What went wrong: explaining counterexamples. In: SPIN, pp. 121–135 (2003)
47.
Groce, A., Visser, W.: Heuristics for model checking Java programs. STTT 6(4), 260–276 (2004)CrossRef
48.
Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Computer Aided Verification—23rd International Conference, Proceedings, pp. 396–411. Springer, Berlin (2011)
49.
Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Proceedings of the Formal Methods in Computer-Aided Design, pp. 1–9 (2008)
50.
Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. High. Order Symb. Comput. 13(4), 315–353 (2000)MATHCrossRef
51.
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder (1998)
52.
Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theor. Comput. Sci. 319(3), 239–257 (2008)MathSciNetCrossRef
53.
Henzinger, T.A.: The theory of hybrid automata. Theor. Comput. Sci 138, 3–34 (1995)MATHCrossRef
54.
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)
55.
Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Model Checking Software: 11th International SPIN, Workshop, pp. 76–91 (2004)
56.
IEEE Standard 1076–2008: VHDL Language Reference Manual. Technical report, Institute of Electrical and Electronics Engineers (2009)
57.
58.
Iosif, R.: Symmetry reductions for model checking of concurrent dynamic software. STTT 6(4), 302–319 (2004)MathSciNetCrossRef
59.
Iosif, R., Dwyer, M.B., Hatcliff, J.: Translating Java for multiple model checkers: the Bandera back-end. Formal Methods Syst. Des. 26(2), 137–180 (2005)MATHCrossRef
60.
Specification and description language. Technical report, International Telecommunication Union, November 1988. ITU Recommendation Z.100
61.
Kahsai, T., Ge, Y., Tinelli, C.: Instantiation-based invariant discovery. In: Bobaru, M., Havelundand, K., Holzmann, G., Joshi, R. (eds.) Proceedings of the 3rd NASA Formal Methods Symposium (Pasadena, CA, USA). Lecture Notes in Computer Science, vol. 6617, pp. 192–207. Springer, Berlin (2011)
62.
Khurshid, S., Pǎsǎreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of TACAS, pp. 553–568 (2003)
63.
Kwiatkowska, M.: Model checking for probability and time: from theory to practice. In: Proceedings 18th Annual IEEE Symposium on Logic in Computer Science (LICS’03), pages 351–360. IEEE Computer Society Press, New York (2003). Invited Paper
64.
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11), pp. 585–591 (2011)
65.
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006)CrossRef
66.
67.
68.
69.
McMillan, K.L.: Circular compositional reasoning about liveness. Technical Report 1999–02, Cadence Berkeley Labs, Berkeley, CA 94704 (1999)
70.
71.
72.
McMillan, K.L.: Applications of Craig interpolants in model checking. In: Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, Proceedings, pp. 1–12 (2005)
73.
Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)CrossRef
74.
Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: Proceedings of ICCAD, vol. 2006, pp. 836–843 (2011)
75.
Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., de Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. In: ECCB’08 Proceedings, Seventh European Conference on Computational Biology, pp. 227–233 (2008)
76.
Musuvathi, M., Qadeer, S.: Chess: Systematic stress testing of concurrent software. In LOPSTR, pp. 15–16 (2006)
77.
Orwick, P., Smith, G.: Developing Drivers with the Windows Driver Foundation. Microsoft Press, Redmond (2007)
78.
Owens, N., Timmis, J., Greensted, A., Tyrrell, A.: Modelling the tunability of early T cell signalling events. In: 7th International Conference on Artificial Immune Systems (ICARIS’08), pp. 12–23 (2008)
79.
Pǎsǎreanu, C., Dwyer, M., Huth, M.: Assume-guarantee model checking of software: a comparative case study. In: Theoretical and Practical Aspects of SPIN Model Checking, pp. 168–183. Springer, Berlin (1999)
80.
Pǎsǎreanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175–205 (2008)CrossRef
81.
Pǎsǎreanu, C.S., Rungta, N., Visser, W.: Symbolic execution with mixed concrete-symbolic solving. In: ISSTA, pp. 34–44 (2011)
82.
Per Bjesse, K.C.: SAT-based verification without state space traversal. In: International Conference on Formal Methods in Computer Aided Design (2000)
83.
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57 (1977)
84.
Pratt, V.R.: Anatomy of the Pentium bug. In: Proceedings of the 6th International Joint Conference on Theory and Practice of Software Development, pp. 97–107 (1995)
85.
Pǎsǎreanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: Proceedings of ISSTA (2008)
86.
Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: International Symposium on Programming, 5th Colloquium, Proceedings, pp. 337–351 (1982)
87.
Robby, M.B.D., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. ACM SIGSOFT Softw. Eng. Notes 28(5), 267–276 (2003)
88.
Sutherland, S., Davidmann, S., Flake, P.: System Verilog for Design. Springer, Berlin (2006)
89.
Thomas, D.E., Moorby, P.R.: The Verilog Hardware Description Language. Kluwer, Norwell (1998)MATH
90.
Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 133–192 (1990)
91.
Tillmann, N., De Halleux, J.: Pex: white box test generation for .NET. In: TAP, pp. 134–153. Springer, Berlin (2008)
92.
Tkachuk, O., Dwyer, M.B., Pǎsǎreanu, C.S.: Automated environment generation for software model checking. In: ASE, pp. 116–129 (2003)
93.
94.
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science, pp. 332–344 (1986)
95.
Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)CrossRef
96.
Wang, J., Zhou, H.: An efficient incremental algorithm for min-area retiming. In: Design Automation Conference (2008)
97.
Xie, T., Tillmann, N., de Halleux, P., Schulte, W.: Fitness-guided path exploration in dynamic symbolic execution. In: Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2009), pp. 359–368 (2009)
Metadaten
Titel
The hidden models of model checking
verfasst von
Willem Visser
Matthew B. Dwyer
Michael Whalen
Publikationsdatum
01.10.2012
Verlag
Springer-Verlag
Erschienen in
Software and Systems Modeling / Ausgabe 4/2012
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-012-0281-9

Weitere Artikel der Ausgabe 4/2012

Software and Systems Modeling 4/2012 Zur Ausgabe

Expert’s Voice

What makes a good process model?

Expert's Voice

The quest for runware: on compositional, executable and intuitive models

Editorial

The journal on Software and Systems Modeling Matures

Expert’s Voice

Aspects of abstraction in software development

Regular Paper

Modeling robustness behavior using aspect-oriented modeling to support robustness testing of industrial systems

Expert's Voice

Lessons learned from building model-driven development tools

Premium Partner

    Bildnachweise