Compositional reasoning for port-based distributed systems

摘要

Many distributed systems using IP-based communication protocols consist of chains of components that run concurrently and communicate asynchronously with their neighbours through ports. We present a compositional reasoning method using model checking and theorem proving to verify liveness properties of a communication protocol for chains of connections consisting of an unknown number of components. We outline how our method is used to verify properties of the call protocol of AT&T's Distributed Feature Composition (DFC) architecture.