Disciplined structured communications with disciplined runtime adaptation

作者：Di Giusto Cinzia; Perez Jorge A^*

来源：Science of Computer Programming, 2015, 97: 235-265.

DOI：10.1016/j.scico.2014.04.017

• Types for structured communications
• Session types
• Process calculi
• Runtime adaptation
• Adaptable processes

Session types offer a powerful type-theoretic foundation for the analysis of structured communications, as commonly found in service-oriented systems. They are defined upon core programming calculi which offer only limited support for expressing requirements related to runtime adaptation. This is unfortunate, as service-oriented systems are increasingly being deployed upon highly dynamic infrastructures in which such requirements are central concerns. In previous work, we developed a process calculi framework of adaptable processes, in which concurrent processes can be replaced, suspended, or discarded at runtime. In this paper, we propose a session type discipline for a calculus with adaptable processes. Our typed framework offers a simple alternative for integrating runtime adaptation mechanisms in the modeling and analysis of structured communications. We show that well-typed processes enjoy safety and consistency properties: while the former property ensures the absence of communication errors at runtime, the latter guarantees that active session behavior is never disrupted by adaptation actions.

• 出版日期2015-1-1