MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Asynchronous Distributed Monitoring for Multiparty Session Enforcement
Tzu-Chun CHEN , Laura BOCCHI , Pierre-Malo DENIÉLOU , Kohei HONDA , Nobuko YOSHIDA
6th International Symposium on Trustworthy Global Computing (TGC 2011) p. 25 - 45

We propose a formal model of runtime safety enforcement for largescale, cross-language distributed applications with possibly untrusted endpoints. The underlying theory is based on multiparty session types with logical assertions (MPSA), an expressive protocol specification language that supports runtime validation through monitoring. Our method starts from global specifications based on MPSAs which the participants should obey. Distributed monitors use local specifications, projected from global specifications, to detect whether the interactions are well-behaved, and take appropriate actions, such as suppressing illegal messages. We illustrate the design of our model with examples from real-world distributed applications. We prove monitor transparency, communication conformance, and global session fidelity in the presence of possibly unsafe endpoints.

@inproceedings{CBDHY2011,
  author = {Tzu-Chun Chen and Laura Bocchi and Pierre-Malo Deniélou and Kohei Honda and Nobuko Yoshida},
  title = {{Asynchronous Distributed Monitoring for Multiparty Session Enforcement}},
  booktitle = {6th International Symposium on Trustworthy Global Computing},
  series = {LNCS},
  volume = {7173},
  pages = {25--45},
  publisher = {Springer},
  year = 2011
}
@inproceedings{CBDHY2011,
  author = {Tzu-Chun Chen and Laura Bocchi and Pierre-Malo Deniélou and Kohei Honda and Nobuko Yoshida},
  title = {{Asynchronous Distributed Monitoring for Multiparty Session Enforcement}},
  booktitle = {6th International Symposium on Trustworthy Global Computing},
  series = {LNCS},
  volume = {7173},
  pages = {25--45},
  publisher = {Springer},
  doi = "10.1007/978-3-642-30065-3_2",
  year = 2011
}