Practical Abstractions for Automated Verification of Message Passing Concurrency

Wytse Oortwijn, Marieke Huisman

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)

    Abstract

    Distributed systems are notoriously difficult to develop correctly, due to the concurrency in their communicating subsystems. Several techniques are available to help developers to improve the reliability of message passing software, including deductive verification and model checking. Both these techniques have advantages as well as limitations, which are complementary in nature. This paper contributes a novel verification technique that combines the strengths of deductive and algorithmic verification to reason elegantly about message passing concurrent programs, thereby reducing their limitations. Our approach allows to verify data-centric properties of message passing programs using concurrent separation logic (CSL), and allows to specify their communication behaviour as a process-algebraic model. The key novelty of the approach is that it formally bridges the typical abstraction gap between programs and their models, by extending CSL with logical primitives for proving deductively that a program refines its process-algebraic model. These models can then be analysed via model checking, using mCRL2, to reason indirectly about the program’s communication behaviour. Our verification approach is compositional, comes with a mechanised correctness proof in Coq, and is implemented as an encoding in Viper.

    Original languageEnglish
    Title of host publicationIntegrated Formal Methods - 15th International Conference, IFM 2019, Proceedings
    EditorsWolfgang Ahrendt, Silvia Lizeth Tapia Tarifa
    PublisherSpringer
    Pages399-417
    Number of pages19
    ISBN (Electronic)978-3-030-34968-4
    ISBN (Print)978-3-030-34967-7
    DOIs
    Publication statusPublished - 22 Nov 2019
    Event15th International Conference on Integrated Formal Methods, IFM 2019 - Western Norway University of Applied Sciences, Bergen, Norway
    Duration: 2 Dec 20196 Dec 2019
    Conference number: 15

    Publication series

    NameLecture Notes in Computer Science
    Volume11918

    Conference

    Conference15th International Conference on Integrated Formal Methods, IFM 2019
    Abbreviated titleIFM
    CountryNorway
    CityBergen
    Period2/12/196/12/19

      Fingerprint

    Cite this

    Oortwijn, W., & Huisman, M. (2019). Practical Abstractions for Automated Verification of Message Passing Concurrency. In W. Ahrendt, & S. L. Tapia Tarifa (Eds.), Integrated Formal Methods - 15th International Conference, IFM 2019, Proceedings (pp. 399-417). (Lecture Notes in Computer Science; Vol. 11918). Springer. https://doi.org/10.1007/978-3-030-34968-4_22