普适服务编排的类型和效果

Types and Effects of Pervasive Service Choreography

提出一种扩展的lambda演算方法并给出相应类型的系统.基于扩展的lambda演算可建立服务模型,采用形式化方法,将服务内部流程抽象为函数概念,引入效果系统来记录服务的动作属性,推导服务动作操作集以验证服务编排是否满足用户所定义的规范,最后通过Coq实验来验证该方法的可行性.

This paper presents an extended lambda calculus method and gives out the corresponding the type system.This service model is based on extended lambda calculus.In our paper,we use the formal method,abstract the service internal process as a function, introduce the effect system to record the action property, and derive the operation set of service actions to verify whether the service choreography meets specifications defined by users.Finally, we verify the practicability of the method by Coq.