Top

Published in:

2018 | OriginalPaper | Chapter

Static Code Verification Through Process Models

Authors : Sebastiaan Joosten, Marieke Huisman

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

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In this extended abstract, we combine two techniques for program verification: one is Hoare-style static verification, and the other is model checking of state transition systems. We relate the two techniques semantically through the use of a ghost variable. Actions that are performed by the program can be logged into this variable, building an event structure as its value. We require the event structure to grow incrementally by construction, giving it behavior suitable for model checking. Invariants specify a correspondence between the event structure and the program state. The combined power of model checking and static code verification with separation logic based reasoning, gives a new and intuitive way to do program verification. We describe our idea in a tool-agnostic way: we do not give implementation details, nor do we assume that the static verification tool to which our idea might apply is implemented in a particular way.

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 ByMC: Byzantine Model Checker

next chapter Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems

Because how validity is defined in the next section, a process defined as \(A = A\) is equivalent to the process for which no event structures are valid, not even the empty one.

Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353–367. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_28CrossRefMATH

Amighi, A.: Specification and verification of synchronisation classes in Java: a practical approach. Ph.D. thesis, University of Twente (2018)

Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127–131. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_9CrossRef

Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233–248. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74061-2_15CrossRef

Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: component reasoning for concurrent objects. J. Logic Algebraic Program. 81(3), 227–256 (2012). https://doi.org/10.1016/j.jlap.2012.01.003, The 22nd Nordic Workshop on Programming Theory (NWPT 2010)

Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 315–331. Springer, Heidelberg (2008)CrossRef

Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978). https://doi.org/10.1145/359576.359585CrossRefMATH

Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. CoRR abs/1405.4028 (2014). http://arxiv.org/abs/1405.4028

Lamport, L., Owicki, S.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982). https://www.microsoft.com/en-us/research/publication/proving-liveness-properties-concurrent-programs/

10.

Oortwijn, W., Blom, S., Huisman, M.: Future-based static analysis of message passing programs. In: PLACES, pp. 65–72 (2016)

11.

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_12CrossRef

12.

Pratt, V.: Modeling concurrency with partial orders. Int. J. Parallel Program. 15(1), 33–71 (1986). https://doi.org/10.1007/BF01379149MathSciNetCrossRefMATH

13.

Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundam. Inf. 63(4), 385–410 (2004). http://dl.acm.org/citation.cfm?id=2370686.2370691

14.

Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_18CrossRef

15.

Vafeiadis, V.: Formal reasoning about the C11 weak memory model. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, pp. 1–2. ACM (2015)

Title: Static Code Verification Through Process Models
Authors: Sebastiaan Joosten
Marieke Huisman
Publisher: Springer International Publishing
Book: Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems
Print ISBN: 978-3-030-03423-8

Electronic ISBN: 978-3-030-03424-5

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-03424-5_23

Springer Professional

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