Research On Description And Verification Of Traffic Web Services Based On Pi-Calculus

At present,the focus of urban transportation systems is on how to set up traffic system in the Internet environment,how to realize resources-sharing and co-operation in wide area,and how to enable urban transportation system continue to work in the face of all kinds of accidents,failures,which means how to empower urban transportation system Survivability. Traditional software technology system can not effectively adapt to the complexity,varied distribution and heterogeneity emerged in the development of urban transport system,and become a constraint in its development.This paper introduces the Web services technology under Internet environment into urban transportation systems for traffic guidance system construction and maintenance.Web services rely on Internet XML-RPC implementation,with advantages such as open standards,platform independence,simplicity,and readable message.It can be applied to achieve cross-plat form,interoperable distributed applications and take into account the reusability of existing system.First of all,this paper gives traffic collaborative Web services architecture based on Web services,and interprets the way of service cooperation with the example of co-transport system.The dynamic combination of Web services enable the system to realize services system re-configuration based on environmental need,and thus enhances survivability of the system.Second,based on that Pi-Calculus has the ability to create a new channel,the Pi-Calculus can be used to describe the ever-changing and complicated system Based on the Pi-Calculus theory,this paper formalizes Pi-Calculus theory to describe the co-emergency transport system and its portfolio of Web services model.Finally,this paper uses the architecture for the development and the implementation of traffic cooperation Web services of the research group,and then through operational semantics of Pi-Calculus,automatic deduction,and other theories to determine the degree of the compatibility between Web services interaction using quantitative calculation.This method can determine under which circumstances services can be normal interacted,and under which circumstances services can not be interacted.This is of great significance for the right combination and monitor of services.