Top

Hint

Swipe to navigate through the chapters of this book

Published in:

Read chapter Read first chapter

2018 | OriginalPaper | Chapter

On Models and Code

A Unified Approach to Support Large-Scale Deductive Program Verification

Author : Marieke Huisman

Published in: Leveraging Applications of Formal Methods, Verification and Validation. Modeling

Publisher: Springer International Publishing

Abstract

Despite the substantial progress in the area of deductive program verification over the last years, it still remains a challenge to use deductive verification on large-scale industrial applications. In this abstract, I analyse why this is case, and I argue that in order to solve this, we need to soften the border between models and code. This has two important advantages: (1) it would make it easier to reason about high-level behaviour of programs, using deductive verification, and (2) it would allow to reason about incomplete applications during the development process. I discuss how the first steps towards this goal are supported by verification techniques within the VerCors project, and I will sketch the future steps that are necessary to realise this goal.

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!

inform now

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!

inform now

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!

inform now

previous chapter Why Programming Must Be Supported by Modeling and How

next chapter Type Theory as a Framework for Modelling and Programming

Of course, a similar argument can be made here, but the advantage is that if the annotated code is available, correctness can be reverified by other tools.

Abrial, J.-R.: Modeling in Event-B – System and Software Engineering. Cambridge University Press (2010)

Amighi, A., Blom, S., Huisman, M.: VerCors: a layered approach to practical verification of concurrent software. In PDP, pp. 495–503 (2016)

Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1) (2015)

Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_1 CrossRef

Bjørner, D.: The vienna development method (VDM). In: Blum, E.K., Paul, M., Takasu, S. (eds.) Mathematical Studies of Information Processing. LNCS, vol. 75, pp. 326–359. Springer, Heidelberg (1979). https://doi.org/10.1007/3-540-09541-1_33 CrossRef

Bowen, J.P., Olderog, E.-R., Fränzle, M., Ravn, A.P.: Developing correct systems. In: Fifth Euromicro Workshop on Real-Time Systems, RTS 1993, Oulu, Finland, 22–24 June 1993, Proceedings, pp. 176–187. IEEE (1993)

Brahmi, A., Delmas, D., Essousi, M.H., Randimbivololona, F., Atki, A., Marie, T.: Formalise to automate: deployment of a safe and cost-efficient process for avionics software. In: Embedded Real-Time Software and Systems (ERTS \(^2\)) (2018)

Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing 1974, pp. 308–312. Elsevier, North-Holland (1974)

Dalvandi, M., Butler, M.J., Rezazadeh, A.: Transforming Event-B models to Dafny contracts. In: Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), Volume 72 of Electronic Communications of the EASST (2015)

10.

Dawes, J.: The VDM-SL Reference Guide. Pitman (1991)

11.

de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273–289. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_16 CrossRef

12.

Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) CrossRef

13.

Huisman, M., Blom, S., Darabi, S., Safari, M.: Program correctness by transformation. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11244, pp. 365–380. Springer, Cham (2018)

14.

Huisman, M., Klebanov, V., Monahan, R., Tautschnig, M.: VerifyThis 2015 a program verification competition. Int. J. Softw. Tools Technol. Transfer (2016)

15.

International Organisation for Standardization. Information technology–Programming languages, their environments and system software interfaces–Vienna Development Method-Specification Language–Part 1: Base language, December 1996. ISO/IEC 13817–1

16.

International Organisation for Standardization. Information technology–Z Formal Specification Notation-Syntax, Type System and Semantics (2000). ISO/IEC 13568:2002

17.

Joosten, S.J.C., Oortwijn, W., Safari, M., Huisman, M.: An exercise in verifying sequential programs with VerCors. In: Summers, A.J. (ed.) 20th Workshop on Formal Techniques for Java-like Programs (FTfJP) (2018)

18.

Jung, R., et al.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637–650. ACM (2015)

19.

Kästner, D., et al.: CompCert: practical experience on integrating and qualifying a formally verified optimizing compiler. In: ERTS 2018: Embedded Real Time Software and Systems. SEE (2018)

20.

Meyer, B.: Object-Oriented Software Construction, 2nd Edn. Prentice-Hall (1997)

21.

O’Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007) MathSciNetCrossRef

22.

Olderog, E.-R., Rössig, S.: A case study in transformational design of concurrent systems. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993. LNCS, vol. 668, pp. 90–104. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56610-4_58 CrossRef

23.

Oortwijn, W., Blom, S., Gurov, D., Huisman, M., Zaharieva-Stojanovski, M.: An abstraction technique for describing concurrent program behaviour. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 191–209. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_12 CrossRef

24.

Partsch, H.: Specification and Transformation of Programs - A Formal Approach to Software Development. Texts and Monographs in Computer Science. Springer, Heidelberg (1990). https://doi.org/10.1007/978-3-642-61512-2

25.

Penninckx, W., Mühlberg, J.T., Smans, J., Jacobs, B., Piessens, F.: Sound formal verification of Linux’s USB BP keyboard driver. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 210–215. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28891-3_21 CrossRef

26.

Tran-Jørgensen, P.W.V., Larsen, P.G., Leavens, G.T.: Automated translation of VDM to JML-annotated Java. STTT 20(2), 211–235 (2018) CrossRef

27.

Zaharieva-Stojanovski, M.: Closer to reliable software: verifying functional behaviour of concurrent programs. Ph.D. thesis, University of Twente (2015)

28.

Zhang, D.: From concurrent state machines to reliable multi-threaded Java code. Ph.D. thesis, Technische Universiteit Eindhoven (2018)

Title: On Models and Code
Author: Marieke Huisman
Publisher: Springer International Publishing
Book: Leveraging Applications of Formal Methods, Verification and Validation. Modeling
Print ISBN: 978-3-030-03417-7

Electronic ISBN: 978-3-030-03418-4

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-03418-4_7

Springer Professional

Hint

Swipe to navigate through the chapters of this book

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner