Skip to main content
Top

2011 | OriginalPaper | Chapter

5. Execution-Based Model Checking for High-Level Designs

Authors : Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta

Published in: High-Level Verification

Publisher: Springer New York

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In this chapter, we present an high-level property checking approach. We begin with a general description of verification of concurrent programs, and then describe it for a high-level language called SystemC [78]. In this approach, we start with a design written in SystemC, and then use model checking techniques to verify that the design satisfies a given property such as the absence of deadlocks or assertion violations.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

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!

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!

Literature
27.
go back to reference Cai, L., Gajski, D.: Transaction Level Modeling: an overview. In: Proceedings of International Conference on Hardware-Software Codesign and System Synthesis (CODES+ISSS) (2003) Cai, L., Gajski, D.: Transaction Level Modeling: an overview. In: Proceedings of International Conference on Hardware-Software Codesign and System Synthesis (CODES+ISSS) (2003)
46.
go back to reference Dill, D.L.: The murphi verification system. In: CAV ’96: Proceedings of the 8th International Conference on Computer Aided Verification, pp. 390–393. Springer-Verlag, London, UK (1996) Dill, D.L.: The murphi verification system. In: CAV ’96: Proceedings of the 8th International Conference on Computer Aided Verification, pp. 390–393. Springer-Verlag, London, UK (1996)
57.
go back to reference Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (2005) Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (2005)
69.
go back to reference Girkar, M., Polychronopoulos, C.D.: Automatic extraction of functional parallelism from ordinary programs. IEEE Transaction on Parallel Distributed Systems (1992) Girkar, M., Polychronopoulos, C.D.: Automatic extraction of functional parallelism from ordinary programs. IEEE Transaction on Parallel Distributed Systems (1992)
71.
go back to reference Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (1997) Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (1997)
78.
go back to reference Grötker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers (2002) Grötker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers (2002)
86.
89.
go back to reference Helmstetter, C., Maraninchi, F., Maillet-Contoz, L., Moy, M.: Automatic generation of schedulings for improving the test coverage of Systems-on-a-Chip. In: FMCAD ’06: Proceedings of the Formal Methods in Computer Aided Design, pp. 171–178. IEEE Computer Society, Washington, DC, USA (2006). DOI http://dx.doi.org/10.1109/FMCAD.2006.10 Helmstetter, C., Maraninchi, F., Maillet-Contoz, L., Moy, M.: Automatic generation of schedulings for improving the test coverage of Systems-on-a-Chip. In: FMCAD ’06: Proceedings of the Formal Methods in Computer Aided Design, pp. 171–178. IEEE Computer Society, Washington, DC, USA (2006). DOI http://​dx.​doi.​org/​10.​1109/​FMCAD.​2006.​10
103.
go back to reference Kahlon, V., Gupta, A., Sinha, N.: Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. In: CAV ’06: Proceedings of the 18th international conference on Computer Aided Verification, pp. 286–299 (2006) Kahlon, V., Gupta, A., Sinha, N.: Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. In: CAV ’06: Proceedings of the 18th international conference on Computer Aided Verification, pp. 286–299 (2006)
114.
go back to reference Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware/software partitioning. In: Proceedings of Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) (2005) Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware/software partitioning. In: Proceedings of Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) (2005)
145.
go back to reference Meftali, S., Vennin, J., Dekeyser, J.L.: A fast SystemC simulation methodology for Multi-Level IP/SoC design. In: IFIP International Workshop on IP Based SoC Design (2003) Meftali, S., Vennin, J., Dekeyser, J.L.: A fast SystemC simulation methodology for Multi-Level IP/SoC design. In: IFIP International Workshop on IP Based SoC Design (2003)
153.
go back to reference Moy, M., Maraninchi, Maillet-Contoz: Lussy: A toolbox for the analysis of Systems-on-a-Chip at the Transactional Level. In: Proceedings of International Conference on Application of Concurrency to System Design (ACSD) (2005) Moy, M., Maraninchi, Maillet-Contoz: Lussy: A toolbox for the analysis of Systems-on-a-Chip at the Transactional Level. In: Proceedings of International Conference on Application of Concurrency to System Design (ACSD) (2005)
174.
go back to reference Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: CAV ’05: Proceedings of the 17th international conference on Computer Aided Verification, pp. 82–97 (2005) Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: CAV ’05: Proceedings of the 17th international conference on Computer Aided Verification, pp. 82–97 (2005)
184.
go back to reference Sen, A., Garg, V.K.: Formal verification of simulation traces using computation slicing. IEEE Transactions on Computers (2007) Sen, A., Garg, V.K.: Formal verification of simulation traces using computation slicing. IEEE Transactions on Computers (2007)
186.
go back to reference Shyamasundar, R., Doucet, F., Gupta, R., Kruger, I.: Compositional reactive semantics of SystemC and verification with RuleBase. In: Proceedings of the GM R&D Workshop (2007) Shyamasundar, R., Doucet, F., Gupta, R., Kruger, I.: Compositional reactive semantics of SystemC and verification with RuleBase. In: Proceedings of the GM R&D Workshop (2007)
201.
go back to reference Vardi, M.Y.: Formal techniques for SystemC verification. In: DAC ’07: Proceedings of the 44th annual conference on Design Automation (2007) Vardi, M.Y.: Formal techniques for SystemC verification. In: DAC ’07: Proceedings of the 44th annual conference on Design Automation (2007)
205.
go back to reference Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: TACAS ’08: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 382–396 (2008) Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: TACAS ’08: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 382–396 (2008)
Metadata
Title
Execution-Based Model Checking for High-Level Designs
Authors
Sudipta Kundu
Sorin Lerner
Rajesh K. Gupta
Copyright Year
2011
Publisher
Springer New York
DOI
https://doi.org/10.1007/978-1-4419-9359-5_5