nach oben

Erschienen in:

2014 | OriginalPaper | Buchkapitel

A Framework for Verification of SystemC Designs Using SystemC Waiting State Automata

verfasst von : Nesrine Harrath, Bruno Monsuez, Kamel Barkaoui

Erschienen in: Integration of Reusable Systems

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

The SystemC waiting-state automaton is a compositional abstract formal model for verifying properties of SystemC at the transaction level within a delta-cycle: the smallest simulation unit time in SystemC. In this chapter, how to extract automata for SystemC components where we distinguish between threads and methods in SystemC. Then, we propose an approach based on a combination of symbolic execution and computing fixed points via predicate abstraction to infer relations between predicates generated during symbolic execution. Finally, we define how to apply model checking to prove the correctness of the abstract analysis.

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 An Institution for Alloy and Its Translation to Second-Order Logic

Nächstes Kapitel Formal MDE-Based Tool Development

Nur mit Berechtigung zugänglich

a Galois connection is a pair of functions \((\alpha ,\gamma )\) satisfying \(\alpha (\gamma (\widetilde{s}))= \widetilde{s}\) and \(\varphi \Rightarrow \gamma (\alpha (\varphi )\)). Given \(\gamma \), \(\alpha \) is implicitly defined by \(\alpha (\varphi )=\cap \{\widetilde{s}\in \widetilde{S}| \varphi \Rightarrow \gamma (\widetilde{s})\}.\)

Main page of the SystemC Initiative. http://www.systemc.org

Drechsler, R., Große, D.: Reachability analysis for formal verification of SystemC. In: Euromicro Symposium on Digital Systems Design, pp. 337–340 (2002)

Drechsler, R., Große, D.: Formal verification of LTL formulas for SystemC designs. In: IEEE International Symposium on Circuits and Systems, vol. 25, pp. 45–248 (2003)

Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware/software partitioning. In: the Third ACM and IEEE International Conference on Formal Methods and Models for Co-Design, pp. 101–110 (2005)

Shyamasundar, R.K., Doucet, F., Gupta, R., Kruger, I.H.: Compositional Reactive Semantics of SystemC and Verification in RuleBase. In: Proceedings of the GM R &D Workshop, pp. 227–243. Bangalore, India (2007)

Harrath, N., Monsuez, B.: Compositional Reactive Semantics of System-Level Designs Written in SystemC and Formal Verification with Predicate Abstraction. accepted in the International Journal of Critical Computer-Based Systems (IJCCBS) (2013)

Plotkin, G.D.: A structural approach to operational semantics. Logic Algebraic Program. 60–61, pp. 17–139 (2004)

Havelund, K., Pressburger, T.: Model checking Java programs using Java pathfinder. Int. J. Softw. Tools Technol. Transfer (STTT) 2(4), 366–381 (2000)CrossRefMATH

Mueller, W., Ruf, J., Rosenstiel, W.: SystemC Methodologies and Applications. Kluwer Academic Publishers, Boston (2003)

10.

Zhang, Y., Védrine, F., Monsuez, B.: SystemC waiting-state automata. In: On First International Workshop on Verification and Evaluation of Computer and Communication Systems, pp. 5–6. eWiC, BCS (2007)

11.

Harrath, N., Monsuez, B.: Timed SystemC waiting-state automata. In: On Third International Workshop on Verification and Evaluation of Computer and Communication Systems. eWiC, BCS (2009)

12.

King, J.C.: Symbolic execution and program testing. Commun. ACM (Assoc. Comput. Mach.) 19(7), 385–394 (1976)

13.

Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of the 29th Annual ACM Symposium on Principles and Programming Languages (POPL), pp. 191–202 (2002)

14.

Bubel, R., \(H\ddot{a} hnle\), R., Weiße, B.: Abstract interpretation of symbolic execution with explit state updates. In: On the International Symposia on Formal Methods for Components and Objects, pp. 247–277 (2008)

15.

Clarke, E., Grumberg, O., Talupur, M., Wang, D.: High level verification of control intensive systems using predicate abstraction. In: Proceedings of First ACM and IEEE International Conference on Formal Methods and Models for Co-Design, IEEE Computer, Society, 25 Sept (2004)

16.

Chaki, S., Clarke, E., Große, A., Strichman, O.: Abstraction with Minimum Predicates. Springer, Berlin/Heidelberg (2003)

17.

Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Symposium on Principles of Programming Languages (POPL) (2005)

18.

Dijkstra, E.W.: A Discipline of Programming. Prentice Hall PTR, Upper Saddle River (1997)

19.

Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) Proceedings, 3rd Asian Symposium on Programming languages and Systems (APLAS). 3780 of LNCS, pp. 119–134 (2002)

20.

Schmitt, P.H., Weiß, B.: Inferring invariants by symbolic execution. In: Proceedings of the 4th International Verification, Workshop (VERIFY’07), pp. 195–210 (2007)

21.

Clarke, E., Grumberg, I., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)

22.

ALUR, R., DILL, D.: Automata for modeling real-time systems. In: Proceedings of 17th International Colloquium on Automata, Languages and Programming (ICALP’90). Lecture Notes in Computer Science, vol. 443, pp. 322–335. Springer, Berlin (1990)

23.

ALUR, R., DILL, D.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)

24.

Große, D., Dreschsler, R.: CheckSyC: An efficient property checker for RTL SystemC designs. In: IEEE International Symposium on Circuits and Systems, pp. 4167–4170 (2005)

25.

Moy, M., Maraninchi, F., Maillet-Contoz, L.: LusSy: A Toolbox for the analysis of systems-on-a-chip at the transactional level. In: IEEE ACSD, pp. 26–35 (2005)

26.

Drechsler, R., Große, D.: CheckSyC: An Efficient Property Checker for RTL SystemC Designs. In: Proceedings of the IEEE International Symposium on Circuits and Systems (ISCAS), vol. 4, pp. 4167–4170 (2005)

27.

Herber, P.: A Framework for Automated HW/SW Co-Verification of SystemC Designs using Timed Automata. Berlin, 145 (2010)

28.

Gawanmeh, A., Habibi, A., Tahar, S.: An executable operational semantics for SystemC using abstract state machines. Technical Report, Concordia University, Department of Electrical and Computer Engineering, pp. 24 (2004)

29.

Habibi, A., Moinudeen, H., Tahar, S.: Generating finite state machines from systemc. In: Gielen, G.G.E. (ed.) DATE Designers’ Forum. European Design and Automation Association, Leuven, Belgium, pp. 6–81 (2006)

30.

Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC designs using a petri-net based representation. In: Proceeding on the Conference on Design, Automation and Test in Europe, pp. 1228–1233 (2005)

31.

Maillet-Contoz, L., Moy, M., Maraninchi, F.: Lussy: a toolbox for the analysis of systems on-a-chip at the transactional level. In: Proceedings of Fifth International Conference on Application of Concurrency to System Design, pp. 26–35 (2005)

32.

Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC designs using a petrinet based representation. In: Proceedings of Design, Automation and Test in Europe, pp. 1228–1233 (2006)

33.

Traulsen, C, Cornet, J., Moy, M., Maraninchi, F.: A SystemC/TLM semantics in promela and its possible applications. In: SPIN, pp. 204–222 (2007)

34.

Herber, P., Fellmuth, J., Glesner, S.: Model checking SystemC designs using timed automata. In: IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System, Synthesis, pp. 131–136 (2008)

Titel: A Framework for Verification of SystemC Designs Using SystemC Waiting State Automata
verfasst von: Nesrine Harrath
Bruno Monsuez
Kamel Barkaoui
Verlag: Springer International Publishing
Buch: Integration of Reusable Systems
Print ISBN: 978-3-319-04716-4

Electronic ISBN: 978-3-319-04717-1

Copyright-Jahr: 2014
DOI: https://doi.org/10.1007/978-3-319-04717-1_4

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"

Premium Partner