Future-based Static Analysis of Message Passing Programs

Dominic Orchard (Editor), Wytse Hendrikus Marinus Oortwijn, Nobuko Yoshida (Editor), Stefan Blom, Marieke Huisman

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.
Original languageUndefined
Pages65-72
Number of pages8
DOIs
StatePublished - Apr 2016

Fingerprint

Message passing
Emergency services
Air traffic control
Model checking
Algebra
Control systems
Industry

Keywords

  • IR-104114
  • EWI-27672

Cite this

Orchard, Dominic (Editor); Oortwijn, Wytse Hendrikus Marinus; Yoshida, Nobuko (Editor); Blom, Stefan; Huisman, Marieke / Future-based Static Analysis of Message Passing Programs.

2016. 65-72.

Research output: Scientific - peer-reviewPaper

@misc{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 = "Dominic Orchard and Oortwijn, {Wytse Hendrikus Marinus} and Nobuko Yoshida and Stefan Blom and Marieke Huisman",
year = "2016",
month = "4",
doi = "10.4204/EPTCS.211.7",
pages = "65--72",

}

Orchard, D (ed.), Oortwijn, WHM, Yoshida, N (ed.), Blom, S & Huisman, M 2016, 'Future-based Static Analysis of Message Passing Programs' pp. 65-72. DOI: 10.4204/EPTCS.211.7

Future-based Static Analysis of Message Passing Programs. / Orchard, Dominic (Editor); Oortwijn, Wytse Hendrikus Marinus; Yoshida, Nobuko (Editor); Blom, Stefan; Huisman, Marieke.

2016. 65-72.

Research output: Scientific - peer-reviewPaper

TY - CONF

T1 - Future-based Static Analysis of Message Passing Programs

AU - Oortwijn,Wytse Hendrikus Marinus

AU - Blom,Stefan

AU - Huisman,Marieke

A2 - Orchard,Dominic

A2 - Yoshida,Nobuko

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 - Paper

SP - 65

EP - 72

ER -

Orchard D, (ed.), Oortwijn WHM, Yoshida N, (ed.), Blom S, Huisman M. Future-based Static Analysis of Message Passing Programs. 2016. Available from, DOI: 10.4204/EPTCS.211.7