(This is a journal version of the conference paper in ICTAC 2014)
Authors
Abstract
The difficulties of verifying distributed programs lie in their inherent nondeterminism and interferences. Rely-Guarantee reasoning is one useful approach to solve this problem for its capability in formally specifying inter-thread interferences. However, modern verification requires better locality and modularity. It is still a great challenge to verify a message-passing program in a modular and composable way.
In this paper, we propose a new reasoning system for message-passing programs. It is a novel logic that supports Hoare style triples to specify and verify distributed programs modularly. We concretize the concept of event traces to represent interactions among distributed agents, and specify behaviors of agents by their local traces with regard to environmental assumptions --- an idea inspired by Rely-Guarantee reasoning. Based on trace semantics, the verification is compositional in both temporal and spatial dimensions. To show validity, we apply our logic to modularly prove several examples.
assumptions. Based on trace semantics, the verification is compositional in both temporal and spatial dimensions. As an example, we show how to modularly verify an implementation of merging network.
Downloads
Journal Version [PDF]