کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
433706 | 1441661 | 2015 | 31 صفحه PDF | دانلود رایگان |
• 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.
Journal: Science of Computer Programming - Volume 97, Part 2, 1 January 2015, Pages 235–265