Practical Abstractions for Automated Verification of Message Passing Concurrency

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.