Jun 04, 2013

Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida

Monitoring Networks through Multiparty Session Types (FORTE 2013)

In large-scale distributed infrastructures, applications are realized through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognized, however, the existing frameworks, relying on centralized verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored π-calculus with the dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralized 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: satisfaction equivalence, local/global safety and transparency, and session fidelity.

Feb 11, 2011

Kohei Honda, Aybek Mukhamedov, Gary Brown, Tzu-Chun Chen, and Nobuko Yoshida

Scribbling Interactions with a Formal Foundation (ICDCIT 2011)

In this paper, we discuss our ongoing endeavor to apply notations and algorithms based on the π-calculus and its theories for the development of large-scale distributed systems. The execution of a large- scale distributed system consists of many structured conversations (or sessions) whose protocols can be clearly and accurately specified using a theory of types for the π-calculus, called session types. The proposed methodology promotes a formally founded, and highly structured, development framework for modeling and building distributed applications, from high-level models to design and implementation to static checking to runtime validation. At the center of this methodology is a formal description language for representing protocols for interactions, called Scribble. We illustrate the usage and theoretical basis of this language through use cases from different application domains.

Jun 09, 2011

Tzu-Chun Chen, Laura Bocchi, Pierre-Malo Denielou, Kohei Honda, and Nobuko Yoshida

Asynchronous Distributed Monitoring for Multiparty Session Enforcement (TGC 2011)

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.

Please reload


T: (+49) 06151-16-27813