To meet the requirements of modeling the new modality of peer-to-peer（P2P）network applications which have been rapidly developing in the Internet recently, a formal description method for modeling multiparty concurr...To meet the requirements of modeling the new modality of peer-to-peer（P2P）network applications which have been rapidly developing in the Internet recently, a formal description method for modeling multiparty concurrent network interactions is studied. The main characteristics and the classifications of P2P systems are discussed. Considering the requirements of P2P application modeling and referring to the component-based modeling thought, a description method based on communicating sequential processes （CSP）is proposed for the P2P network models. By using a CSP process group, this method can describe the dynamic interactive relationship which focuses on multiparty concurrent interaction of P2P systems more advantageously and accurately. The application of nondeterministic semantemes of CSP in describing the interactive relationship of P2P networks is discussed. The advantages and description abilities of the proposed method are demonstrated through the modeling of a new P2P media-on-demand system.展开更多
Communicating Sequential Processes （CSP） is a kind of process algebra, which is suitable for modeling and verifying Web service composition. This paper describes how to model Web service composition with CSP. A set ...Communicating Sequential Processes （CSP） is a kind of process algebra, which is suitable for modeling and verifying Web service composition. This paper describes how to model Web service composition with CSP. A set of rules for translating composition constructor of Business Process Execution Language for Web Services （BPEL4WS） to CSP notations is defined. According to the rules that have been defined, the corresponding translation algorithm is designed and illustrated with examples . The methods for model checking, model verification and model simulation are also introduced.展开更多
Web service （WS） is an emerging software technology, especially acting an important role in cloud computing. The WS choreography description language （WS-CDL） is the standard for modeling the observable behavior o...Web service （WS） is an emerging software technology, especially acting an important role in cloud computing. The WS choreography description language （WS-CDL） is the standard for modeling the observable behavior of WS composition across multiple participants from a global point of view. However, it lacks of a formal semantics and could easily lead to misunderstanding and different implementations. In this paper, the WS-CDL based specifications are formally extracted in a communicating sequential process supporting a formal approach to checking WS models. In addition, formalisms and model checking are explicitly illustrated through a simple but non-trivial example with the help of model checker process analysis toolkit （PAT）.展开更多
基金The National Basic Research Program of China (973 Program)(No.2003CB314801,2009CB320501)
文摘To meet the requirements of modeling the new modality of peer-to-peer（P2P）network applications which have been rapidly developing in the Internet recently, a formal description method for modeling multiparty concurrent network interactions is studied. The main characteristics and the classifications of P2P systems are discussed. Considering the requirements of P2P application modeling and referring to the component-based modeling thought, a description method based on communicating sequential processes （CSP）is proposed for the P2P network models. By using a CSP process group, this method can describe the dynamic interactive relationship which focuses on multiparty concurrent interaction of P2P systems more advantageously and accurately. The application of nondeterministic semantemes of CSP in describing the interactive relationship of P2P networks is discussed. The advantages and description abilities of the proposed method are demonstrated through the modeling of a new P2P media-on-demand system.
基金Supported by the National Natural Science Foun-dation of China(60403027) the Natural Science Foundation of HubeiProvince(2005ABA258) the Open Foundation of State Key La-boratory of Software Engineering (SKLSE05-07)
文摘Communicating Sequential Processes （CSP） is a kind of process algebra, which is suitable for modeling and verifying Web service composition. This paper describes how to model Web service composition with CSP. A set of rules for translating composition constructor of Business Process Execution Language for Web Services （BPEL4WS） to CSP notations is defined. According to the rules that have been defined, the corresponding translation algorithm is designed and illustrated with examples . The methods for model checking, model verification and model simulation are also introduced.
基金supported by the Shanghai Leading Academic Discipline Project (Grant No.J50103)
文摘Web service （WS） is an emerging software technology, especially acting an important role in cloud computing. The WS choreography description language （WS-CDL） is the standard for modeling the observable behavior of WS composition across multiple participants from a global point of view. However, it lacks of a formal semantics and could easily lead to misunderstanding and different implementations. In this paper, the WS-CDL based specifications are formally extracted in a communicating sequential process supporting a formal approach to checking WS models. In addition, formalisms and model checking are explicitly illustrated through a simple but non-trivial example with the help of model checker process analysis toolkit （PAT）.
