nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Efficient Runtime Assertion Checking for Properties over Mathematical Numbers

verfasst von : Nikolai Kosmatov, Fonenantsoa Maurica, Julien Signoles

Erschienen in: Runtime Verification

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

Runtime assertion checking is the discipline of detecting at runtime violations of program properties written as formal code annotations. These properties often include numerical properties, which may rely on either (bounded) machine representations or (unbounded) mathematical numbers. The verification of the former is easier to implement and more efficient at runtime, while the latter are more expressive and often more adequate for writing specifications. This short paper explains how the runtime assertion checker E-ACSL reconciles both approaches by presenting a type system that allows the tool to generate efficient machine-number based code when it is safe to do so, while generating arbitrary-precision code when it is necessary. This type system and the code generator not only handle integers but also rational arithmetics. As far as we know, it is the first runtime verification tool that supports the verification of properties over rational numbers.

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 SharpDetect: Dynamic Analysis Framework for C#/.NET Programs

Nächstes Kapitel BISM: Bytecode-Level Instrumentation for Software Monitoring

https://blog.regehr.org/archives/1091.

See e.g. http://www-users.math.umn.edu/~arnold/disasters/patriot.html.

See e.g. https://en.wikipedia.org/wiki/Vancouver_Stock_Exchange.

https://gmplib.org/.

E-ACSL also supports floating-point constants such as 0.1f but they are excluded here for the sake of simplicity.

Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes 31(3), 25–37 (2006)CrossRef

Kosmatov, N., Signoles, J.: A lesson on runtime assertion checking with frama-C. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 386–399. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40787-1_29CrossRef

Chalin, P.: JML support for primitive arbitrary precision numeric types: definition and semantics. J. Object Technol. 3(6), 57–79 (2004)CrossRef

Chalin, P.: Improving JML: for a safer and more effective language. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 440–461. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_25CrossRef

Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Symposium on Applied Computing (SAC), March 2013

Meyer, B.: Eiffel: The Language. Prentice-Hall, Upper Saddle River (1992)MATH

Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3CrossRef

Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. SECS, vol. 523, pp. 175–188. Springer, Boston (1999). https://doi.org/10.1007/978-1-4615-5229-1_12CrossRef

Dross, C., Filliâtre, J.-C., Moy, Y.: Correct code containing containers. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 102–118. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21768-5_9CrossRef

10.

Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C specification language. http://frama-c.com/acsl.html

11.

Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8CrossRef

12.

Kosmatov, N., Marché, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 461–478. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_32CrossRef

13.

Signoles, J., Kosmatov, N., Vorobyov, K.: E-ACSL, a runtime verification tool for safety and security of C programs. Tool paper. In: International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES), September 2017

14.

Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27, 573–609 (2015)MathSciNetCrossRef

15.

Signoles, J.: E-ACSL: executable ANSI/ISO C specification language. http://frama-c.com/download/e-acsl/e-acsl.pdf

16.

Signoles, J.: From static analysis to runtime verification with Frama-C and E-ACSL, Habilitation thesis, July 2018

17.

Jakobsson, A., Kosmatov, N., Signoles, J.: Rester statique pour devenir plus rapide, plus précis et plus mince. In: Journées Francophones des Langages Applicatifs (JFLA), January 2015. (In French)

18.

ISO: ISO C Standard 1999. Technical report (1999)

19.

Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002)MATH

20.

Vorobyov, K., Signoles, J., Kosmatov, N.: Shadow state encoding for efficient monitoring of block-level properties. In: International Symposium on Memory Management (ISMM), June 2017

21.

Pariente, D., Signoles, J.: Static analysis and runtime assertion checking: contribution to security counter-measures. In: Symposium sur la Sécurité des Technologies de l’Information et des Communications (SSTIC), June 2017

22.

Muller, J., et al.: Handbook of Floating-Point Arithmetic. Birkhäuser, Boston (2010)CrossRef

23.

Richardson, D., Fitch, J.P.: The identity problem for elementary functions and constants. In: International Symposium on Symbolic and Algebraic Computation (ISSAC), July 1994

Titel: Efficient Runtime Assertion Checking for Properties over Mathematical Numbers
verfasst von: Nikolai Kosmatov
Fonenantsoa Maurica
Julien Signoles
Verlag: Springer International Publishing
Buch: Runtime Verification
Print ISBN: 978-3-030-60507-0

Electronic ISBN: 978-3-030-60508-7

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-60508-7_17

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