Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

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 »
InTGC
SeriesLecture Notes in Computer Science
Volume7173
Page(s)25-45
Year2011
PublisherSpringer
ISBN number978-3-642-30064-6
URLhttp://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: TGC_2011.pdf

BibTeX code

@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},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!