Project Overview
This project is aimed at providing a formal grounding of web services, thus enabling formal analysis and verification of web services, especially the composition of web services. Currently we are studying two W3C standards, namely WS-BPEL and WS-CDL.
As a volunteer work, we have translated the WS-CDL specification into Chinese. Here is the Chinese document.
Papers
- Model-checking of Web Services Choreography.
Yang Hongli, Zhao Xiangpeng, Cai Chao, and Qiu Zongyan,
Technical Report (TR pdf). In Proceedings of the 4th IEEE International Workshop on Service-Oriented System Engineering (SOSE 2008), National Central University, Jhongli, Taiwan, China. IEEE CS, 2008 - Correct Channel Passing by Construction. Cai Chao, Qiu Zongyan, Xiangpeng Zhao, and Hongli Yang, In Proceedings of 10th International Conference on Formal Engineering Methods (ICFEM 2008), Japan. LNCS 5256. Spinger, 2008 (pdf)
- An Approach to Checking Choreography with Channel Passing in WS-CDL. Cai Chao and Qiu Zongyan, In Proceedings of 2008 IEEE International Conference on Web Services (ICWS 2008), Beijing, China. IEEE CS, 2008 (pdf)
- A Formal Model of Human Workflow. Xiangpeng Zhao, Zongyan Qiu, Chao Cai, and Hongli Yang, In Proceedings of 2008 IEEE International Conference on Web Services (ICWS 2008), Beijing, China. IEEE CS, 2008 (TR pdf)
- A Formal Model for Channel Passing in Web Service Composition. Chao Cai, Hongli Yang, Xiangpeng Zhao, and Zongyan Qiu, To appear in SCC 2008, 2008 IEEE International Conference on Services Computing, Work in Progress Paper, Honolulu, Hawaii, USA. IEEE CS, 2008
- Reasoning about channel passing in choreography. Hongli Yang, Chao Cai, Liyang Peng, Xiangpeng Zhao, and Zongyan Qiu, In Proceedings of 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), Nanjing, China. IEEE CS, 2008 (TR pdf)
- Verifying BPEL-like Programs with Hoare Logic. Chenguang Luo, Shengchao Qin, and Zongyan Qiu, In Proceedings of 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), Nanjing, China. IEEE CS, 2008 (TR pdf)
- A QoS View of Web Service Choreography. Zhao Xiangpeng, Cai Chao, Yang Hongli, and Qiu Zongyan, In Proc. of 3rd IEEE International Workshop on Service-Oriented System Engineering (SOSE 2007), Hong Kong, China. IEEE CS, 2007
- Exploring the Connection of Choreography and Orchestration with Exception Handling and Finalization/Compensation. Yang Hongli, Zhao Xiangpeng, Cai Chao, and Qiu Zongyan, In Proc. of FORTE 2007, Tallinn, Estonia, 2007. LNCS 4574. Speinger, 2007 ( pdf )
- Towards the Theoretical Foundation of Choreography. Qiu Zongyan, Zhao Xiangpeng, Cai Chao, and Yang Hongli, In Proc. of WWW 2007, Banff, Canada, Jan 2007. ACM, 2007 ( pdf )
- Exploring into the Essence of Choreography. Qiu Zongyan, Cai Chao, Zhao Xiangpeng, and Yang Hongli, Technical Report, Peking Univ., China. ( pdf )
- Type Checking Choreography Description Language. Hongli Yang, Xiangpeng Zhao, Zongyan Qiu, Chao Cai and Geguang Pu, In Proc. of ICFEM 2006, Macao SAR, China. LNCS 4260, Springer, 2006 ( pdf )
- Towards the Formal Model and Verification of Web Service Choreography Description Language. Zhao Xiangpeng, Yang Hongli, and Qiu Zongyan, In Proc. of WS-FM 2006, LNCS 4184, Vienna, Austria. ( pdf )
- A Formal Model for Web Service Choreography Description Language (WS-CDL). Hongli Yang, Xiangpeng Zhao, Zongyan Qiu, Geguang Pu, and Shuling Wang, In Proc. of ICWS 2006, Chicago, USA. IEEE CS, 2006 ( pdf )
- Theoretical Foundation of Scope-based Compensable Flow Language for Web Service. Geguang Pu, Huibiao Zhu, Qiu Zongyan, Shuling Wang, Zhao Xiangpeng, and Jifeng He, In Proc. of FMOODS'06, LNCS 4037, pp. 251¨C266, Springer, 2006. ( pdf )
- Semantics of BPEL4WS-like fault and compensation handling. Qiu Zongyan, Wang Shuling, Pu Geguang, and Zhao Xiangpeng, In Proc. of FM 2005, New Castle, UK, 2005.7. Lecture Notes on Computer Science 3582, pp. 350-365, Springer, 2005. ( pdf )
- Towards the semantics and verification of BPEL4WS. Pu Geguang, Zhao Xiangpeng, Wang Shuling, and Qiu Zongyan, In Proc. of International Workshop on Web Languages and Formal Methods, WLFM 2005, New Castle, UK, 2005.7. ENTCS, Vol. 151, Issue 2, pp.33-52, Elsevier, 2006. ( pdf )
Tools
- Derive Initial Channel Sets: The program is an extention to Pi4SOA. It takes as input a WS-CDL document in ".cdl" or ".cdm", and gives the initial channel sets for each role as result. A paper explaining its mechanism is submitted to ICWS2008. ( download )
- Chor & Role: A Mathematica implementation of the Chor and Role language described in the FORTE'07 paper. ( download )
- CDL2SPIN: Converts a WS-CDL specification into Promela, which is the input language for SPIN. ( download )
- BPEL2UPPAAL: Converts a WS-BPEL specification into the input language of UPPAAL. ( download )
Participants
Prof. Qiu Zongyan, Yang Hongli, Pu Geguang, Zhao Xiangpeng, Wang Shuling, Cai Chao, Peng Liyang