Future-based Static Analysis of Message Passing Programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Message passing is widely used in industry to develop programs consisting of several distributed communicating components. Developing functionally correct message passing software is very challenging due to the concurrent nature of message exchanges. Nonetheless, many safety-critical applications rely on the message passing paradigm, including air traffic control systems and emergency services, which makes proving their correctness crucial. We focus on the modular verification of MPI programs by statically verifying concrete Java code. We use separation logic to reason about local correctness and define abstractions of the communication protocol in the process algebra used by mCRL2. We call these abstractions futures as they predict how components will interact during program execution. We establish a provable link between futures and program code and analyse the abstract futures via model checking to prove global correctness. Finally, we verify a leader election protocol to demonstrate our approach.
LanguageEnglish
Title of host publicationProceedings PLACES 2016
EditorsDominic Orchard, Nobuko Yoshida
Pages65-72
Number of pages8
DOIs
StatePublished - Apr 2016
EventNinth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2016 - Eindhoven, Netherlands
Duration: 8 Apr 20168 Apr 2016
Conference number: 9

Workshop

WorkshopNinth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2016
Abbreviated titlePLACES 16
CountryNetherlands
CityEindhoven
Period8/04/168/04/16
OtherWorkshop affiliated with ETAPS 2016

Fingerprint

Message passing
Static analysis
Emergency services
Network protocols
Air traffic control
Model checking
Algebra
Concretes
Control systems
Industry

Keywords

  • IR-104114
  • EWI-27672

Cite this

Oortwijn, W. H. M., Blom, S., & Huisman, M. (2016). Future-based Static Analysis of Message Passing Programs. In D. Orchard, & N. Yoshida (Eds.), Proceedings PLACES 2016 (pp. 65-72). DOI: 10.4204/EPTCS.211.7
Oortwijn, Wytse Hendrikus Marinus ; Blom, Stefan ; Huisman, Marieke. / Future-based Static Analysis of Message Passing Programs. Proceedings PLACES 2016. editor / Dominic Orchard ; Nobuko Yoshida. 2016. pp. 65-72
@inproceedings{b231409938bd4b9e9fa09c37cd706629,
title = "Future-based Static Analysis of Message Passing Programs",
abstract = "Message passing is widely used in industry to develop programs consisting of several distributed communicating components. Developing functionally correct message passing software is very challenging due to the concurrent nature of message exchanges. Nonetheless, many safety-critical applications rely on the message passing paradigm, including air traffic control systems and emergency services, which makes proving their correctness crucial. We focus on the modular verification of MPI programs by statically verifying concrete Java code. We use separation logic to reason about local correctness and define abstractions of the communication protocol in the process algebra used by mCRL2. We call these abstractions futures as they predict how components will interact during program execution. We establish a provable link between futures and program code and analyse the abstract futures via model checking to prove global correctness. Finally, we verify a leader election protocol to demonstrate our approach.",
keywords = "IR-104114, EWI-27672",
author = "Oortwijn, {Wytse Hendrikus Marinus} and Stefan Blom and Marieke Huisman",
year = "2016",
month = "4",
doi = "10.4204/EPTCS.211.7",
language = "English",
pages = "65--72",
editor = "Dominic Orchard and Nobuko Yoshida",
booktitle = "Proceedings PLACES 2016",

}

Oortwijn, WHM, Blom, S & Huisman, M 2016, Future-based Static Analysis of Message Passing Programs. in D Orchard & N Yoshida (eds), Proceedings PLACES 2016. pp. 65-72, Ninth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2016, Eindhoven, Netherlands, 8/04/16. DOI: 10.4204/EPTCS.211.7

Future-based Static Analysis of Message Passing Programs. / Oortwijn, Wytse Hendrikus Marinus; Blom, Stefan; Huisman, Marieke.

Proceedings PLACES 2016. ed. / Dominic Orchard; Nobuko Yoshida. 2016. p. 65-72.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Future-based Static Analysis of Message Passing Programs

AU - Oortwijn,Wytse Hendrikus Marinus

AU - Blom,Stefan

AU - Huisman,Marieke

PY - 2016/4

Y1 - 2016/4

N2 - Message passing is widely used in industry to develop programs consisting of several distributed communicating components. Developing functionally correct message passing software is very challenging due to the concurrent nature of message exchanges. Nonetheless, many safety-critical applications rely on the message passing paradigm, including air traffic control systems and emergency services, which makes proving their correctness crucial. We focus on the modular verification of MPI programs by statically verifying concrete Java code. We use separation logic to reason about local correctness and define abstractions of the communication protocol in the process algebra used by mCRL2. We call these abstractions futures as they predict how components will interact during program execution. We establish a provable link between futures and program code and analyse the abstract futures via model checking to prove global correctness. Finally, we verify a leader election protocol to demonstrate our approach.

AB - Message passing is widely used in industry to develop programs consisting of several distributed communicating components. Developing functionally correct message passing software is very challenging due to the concurrent nature of message exchanges. Nonetheless, many safety-critical applications rely on the message passing paradigm, including air traffic control systems and emergency services, which makes proving their correctness crucial. We focus on the modular verification of MPI programs by statically verifying concrete Java code. We use separation logic to reason about local correctness and define abstractions of the communication protocol in the process algebra used by mCRL2. We call these abstractions futures as they predict how components will interact during program execution. We establish a provable link between futures and program code and analyse the abstract futures via model checking to prove global correctness. Finally, we verify a leader election protocol to demonstrate our approach.

KW - IR-104114

KW - EWI-27672

U2 - 10.4204/EPTCS.211.7

DO - 10.4204/EPTCS.211.7

M3 - Conference contribution

SP - 65

EP - 72

BT - Proceedings PLACES 2016

ER -

Oortwijn WHM, Blom S, Huisman M. Future-based Static Analysis of Message Passing Programs. In Orchard D, Yoshida N, editors, Proceedings PLACES 2016. 2016. p. 65-72. Available from, DOI: 10.4204/EPTCS.211.7