Disciplined structured communications with disciplined runtime adaptation

•A model of session communications with located and update processes.•A type discipline that ensures absence of communication errors and consistent updates.•Several examples of runtime adaptation in the typed process framework.

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.