In large-scale distributed infrastructures, applications are realised through com-
munications among distributed components. The need for methods for assuring
safe interactions in such environments is recognised, however the existing frame-
works, relying on centralised verification or restricted specification methods, have
limited applicability. This paper proposes a new theory of
monitored
π
-calculus
with dynamic usage of
multiparty session types
(MPST), offering a rigorous foun-
dation for safety assurance of distributed components which asynchronously com-
municate through multiparty sessions. Our theory establishes a framework for
semantically precise decentralised run-time enforcement and provides reasoning
principles over monitored distributed applications, which complement existing
static analysis techniques. We introduce asynchrony through the means of explicit
routers and global queues, and propose novel equivalences between networks, that
capture the notion of interface equivalence, i.e. equating networks offering the
same services to a user. We illustrate our static-dynamic analysis system with an
ATM protocol as a running example and justify our theory with results: satisfac-
tion equivalence, local/global safety and transparency, and session fidelity.