nach oben

Erschienen in:

2011 | OriginalPaper | Buchkapitel

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

verfasst von : Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta

Erschienen in: High-Level Verification

Verlag: Springer New York

Einloggen

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

search-config

KI-gestützte Suche

Aus

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.

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 Verification Using Automated Theorem Provers

Nächstes Kapitel Bounded Model Checking for Concurrent Systems: Synchronous Vs. Asynchronous

Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state-space exploration. Formal Methods System Design 18(2), 97–116 (2001). DOI http://dx.doi.org/10.1023/A:1008767206905

Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI ’01: Proceedings of the 2001 ACM SIGPLAN conference on Programming Language Design and Implementation (2001). URL citeseer.ist.psu.edu/ball01automatic.html

27.

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.

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)

50.

(EDG), E.D.G.: C/C++ Front End (1992). www.edg.com

57.

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)

67.

Ganai, M.K., Gupta, A.: Efficient modeling of concurrent systems in bmc. In: SPIN ’08: Proceedings of the 15th international workshop on Model Checking Software, pp. 114–133. Springer-Verlag, Berlin, Heidelberg (2008). DOI http://dx.doi.org/10.1007/978-3-540-85114-1_10

69.

Girkar, M., Polychronopoulos, C.D.: Automatic extraction of functional parallelism from ordinary programs. IEEE Transaction on Parallel Distributed Systems (1992)

70.

Godefroid, P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Ph.D. thesis, Univerite De Liege (1995). URL citeseer.ist.psu.edu/godefroid95partialorder.html

71.

Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (1997)

77.

Grobe, D., Ebendt, R., Drechsler, R.: Improvements for constraint solving in the SystemC verification library. In: GLSVLSI ’07: Proceedings of the 17th ACM Great Lakes symposium on VLSI, pp. 493–496. ACM, New York, NY, USA (2007). DOI http://doi.acm.org/10.1145/1228784.1228901

78.

Grötker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers (2002)

86.

Habibi, A., Tahar, S.: Design for verification of SystemC Transaction Level Models. In: DATE ’05: Proceedings of the conference on Design, Automation and Test in Europe, pp. 560–565. IEEE Computer Society, Washington, DC, USA (2005). DOI http://dx.doi.org/10.1109/DATE.2005.112

88.

Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Higher Order Symbolic Computation 13(4), 315–353 (2000). DOI http://dx.doi.org/10.1023/A:1026599015809

89.

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

94.

Holzmann, G.J.: The model checker SPIN. Software Engineering 23(5), 279–295 (1997). URL citeseer.ist.psu.edu/holzmann97model.html

95.

Initiative, O.S.: IEEE Standard 1666 SystemC Language Reference Manual (2005). www.systemc.org

103.

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.

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)

115.

Kundu, S., Ganai, M., Gupta, R.: Partial Order Reduction for Scalable Testing of SystemC TLM Designs. In: DAC ’08: Proceedings of the 45th annual conference on Design Automation, pp. 936–941. ACM, New York, NY, USA (2008). DOI http://doi.acm.org/10.1145/1391469.1391706

145.

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)

149.

Microelectronics, S.: Transaction Accurate Communication (TAC) platform (2005). www.greensocs.com/TACPackage

153.

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.

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)

177.

Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Transactions on Programing Language Systems 22(2), 416–430 (2000). DOI http://doi.acm.org/10.1145/349214.349241

184.

Sen, A., Garg, V.K.: Formal verification of simulation traces using computation slicing. IEEE Transactions on Computers (2007)

186.

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)

192.

Swan, S.: Systemc transaction level models and rtl verification. In: DAC ’06: Proceedings of the 43rd annual conference on Design automation, pp. 90–92. ACM, New York, NY, USA (2006). DOI http://doi.acm.org/10.1145/1146909.1146937

201.

Vardi, M.Y.: Formal techniques for SystemC verification. In: DAC ’07: Proceedings of the 44th annual conference on Design Automation (2007)

205.

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)

Titel: Execution-Based Model Checking for High-Level Designs
verfasst von: Sudipta Kundu
Sorin Lerner
Rajesh K. Gupta
Verlag: Springer New York
Buch: High-Level Verification
Print ISBN: 978-1-4419-9358-8

Electronic ISBN: 978-1-4419-9359-5

Copyright-Jahr: 2011
DOI: https://doi.org/10.1007/978-1-4419-9359-5_5

Neuer Inhalt

Bildnachweise

VDI-Icon, Profil Icon, inhalt2, Springer Professional Modul/© Springer Fachmedien Wiesbaden GmbH, Nachhaltigkeitsaward Key Visual/© Cometis AG/Global ESG Monitor | Daniel Rupp | Generiert mit KI, Search Icon, Banner Hanser, Beijing Auto Show 2024: Deutsche Hersteller wollen angreifen./© EKH-Pictures / Generated with AI / Stock.adobe.com, Buchstaben, die aus einem Megaphon kommen/© MicroStockHub/Getty Images/iStock, Digitale Lieferkette/© zapp2photo / stock.adobe.com, Zeitschrift Wissensmanagement Cover, PatentFit-Logo/© Springer Fachmedien Wiesbaden GmbH, Sustainibility Finance/© Robert Kneschke / stock.adobe.com / Springer Fachmedien Wiesbaden GmbH, Zukunftswerkstatt Sales Excellence 2024/© AndreyPopov / Getty Images / iStock, 2023_Antrieb/© supervisuell

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"

Neuer Inhalt

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

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