nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Safety First: About the Detection of Arithmetic Overflows in Hardware Design Specifications

verfasst von : Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler

Erschienen in: Model-Driven Engineering and Software Development

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

This work proposes an alternative hardware design approach that allows the detection of arithmetic overflows at the specification level. The established hardware design approach describes infinite integer types at that level while the model describes finite types. This opens a semantic gap between both levels, which means that arithmetic overflows cannot be detected at the specification level. To address this problem the CompCert integer library is utilized that describes finite integer types as dependent types using the proof assistant Coq. Properties that argue about these finite types can be specified and verified at the specification level. This closes the semantic gap the established hardware design approach suffers from.

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 The Smart Grid Simulation Framework: Model-Driven Engineering Applied to Cyber-Physical Systems

Nächstes Kapitel Systematic Synthesis of Energy-Aware Timing Models in Automotive Software Systems

Note that SystemC is a collection of C++ class libraries designed to describe hardware designs.

The current standard for the C++ programming language is specified in ISO/IEC 14882:2017.

A trap is a software interrupt that is triggered due to an instruction execution, e.g. division-by-zero, by the processor.

C\(\lambda \)aSH: Structural Descriptions of Synchronous Hardware Using Haskell (2010)

Accellera: Accellera Systems Initiative Inc. SystemC Synthesizable Subset (Version 1.5.7) (2016)

Arnout, G.: Systemc standard. In: Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 573–578 (2000)

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004). https://doi.org/10.1007/978-3-662-07964-5

Bornebusch, F., Lüth, C., Wille, R., Drechsler, R.: Integer overflow detection in hardware designs at the specification level. In: 8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD) (2020)

Bornebusch, F., Lüth, C., Wille, R., Drechsler, R.: Towards automatic hardware synthesis from formal specification to implementation. In: Asia and South Pacific Design Automation Conference (ASP-DAC) (2020)

Brady, E., McKinna, J., Hammond, K.: Constructing correct circuits: verification of functional aspects of hardware specifications with dependent types. In: Trends in Functional Programming (TFP), pp. 159–176 (2007)

Brucker, A.D., Wolff, B.: The HOL-OCL book. Technical Report 525, ETH Zurich (2006)

Cabot, J., Clarisó, R., Riera, D.: Verification of UML/OCL class diagrams using constraint programming. In: First International Conference on Software Testing Verification and Validation, ICST, pp. 73–80 (2008)

10.

Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)CrossRef

11.

Coker, Z., Hafiz, M.: Program transformations to fix C integers. In: 35th International Conference on Software Engineering, ICSE 2013, San Francisco, CA, USA, 18–26 May 2013, pp. 792–801 (2013)

12.

Cousot, P.: Formal verification by abstract interpretation. In: NASA Formal Methods - International Symposium, NFM, pp. 3–7 (2012)

13.

Cousot, P., et al.: The astreé analyzer. In: European Symposium on Programming, pp. 21–30 (2005)

14.

Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C - a software analysis perspective. In: International Conference on Software Engineering and Formal Methods, pp. 233–247 (2012)

15.

Dietz, W., Li, P., Regehr, J., Adve, V.S.: Understanding integer overflow in C/C++. ACM Trans. Softw. Eng. Methodol. 25(1), 1–29 (2015)CrossRef

16.

Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: International Conference on Formal Verification of Object-Oriented Software, pp. 10–30 (2010)

17.

Hanna, F.K., Daeche, N.: Dependent types and formal synthesis (1992)

18.

Kuper, J., Baaij, C., Kooijman, M.: Exercises in architecture specification using c\(\lambda \)ash. In: Forum on Specification and Design Languages (FDL) (2010)

19.

Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: Compcert - a formally verified optimizing compiler. In: Embedded Real Time Software and Systems (ERTS) (2016)

20.

Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: European Joint Conferences on Theorey and & Practice of Software, pp. 213–228 (2002)

21.

OMG: Object Management Group Object Constraint Language (OCL) (Version 2.4) (2014)

22.

OMG: Open Management Group System Modeling Language (SysML) (Version 1.6) (2019)

23.

Przigoda, N., Wille, R., Drechsler, R.: Analyzing inconsistencies in UML/OCL models. J. Circ. Syst. Comput. 25(3), 1640021 (2016)CrossRef

24.

Takach, A.: High-level synthesis: status, trends, and future directions. IEEE Des. Test 33(3), 116–124 (2016)CrossRef

25.

Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden, 24–30 May 1995, Tutorial Text. Lecture Notes in Computer Science, vol. 925, pp. 24–52 (1995)

26.

Weilkiens, T.: Systems Engineering with SysML / UML - Modeling, Analysis. Design. Morgan Kaufmann, Burlington (2007)MATH

Titel: Safety First: About the Detection of Arithmetic Overflows in Hardware Design Specifications
verfasst von: Fritjof Bornebusch
Christoph Lüth
Robert Wille
Rolf Drechsler
Verlag: Springer International Publishing
Buch: Model-Driven Engineering and Software Development
Print ISBN: 978-3-030-67444-1

Electronic ISBN: 978-3-030-67445-8

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-67445-8_2

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"