ChenBDHY11 (In proceedings)
|
Author(s) | Tzu-Chun Chen, Laura Bocchi, Pierre-Malo Deniélou, Kohei Honda and Nobuko Yoshida |
Title | « Asynchronous Distributed Monitoring for Multiparty Session Enforcement » |
In | TGC |
Series | Lecture Notes in Computer Science |
Volume | 7173 |
Page(s) | 25-45 |
Year | 2011 |
Publisher | Springer |
ISBN number | 978-3-642-30064-6 |
URL | http://www.di.unito.it/~chen/papers/TGC_2011.pdf |
Abstract |
We propose a formal model of runtime safety enforcement for large-scale, 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. |
Download the complete article: 
@inproceedings{ChenBDHY11,
volume = {7173},
author = {Tzu-Chun Chen and Laura Bocchi and Pierre-Malo Deni{\'e}lou and
Kohei Honda and Nobuko Yoshida},
series = {Lecture Notes in Computer Science},
booktitle = {TGC},
url = {http://www.di.unito.it/~chen/papers/TGC_2011.pdf},
title = {Asynchronous Distributed Monitoring for Multiparty Session
Enforcement},
isbn = {978-3-642-30064-6},
tag = {TGC 2011},
abstract = {We propose a formal model of runtime safety enforcement for
large-scale, 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.},
localfile = {http://www.di.unito.it/~chen/papers/TGC_2011.pdf},
publisher = {Springer},
year = {2011},
pages = {25-45},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
