[1] Alves A,Arkin A,Askary S.Web services business process execution language version 2.0 [EB/OL].http://docs.oasis-open.org/wsbpel/20/OS/wsbpel-v2.0-OS.html.2007-4-11.[2] Diaz G,Pardo J J,et al.Design and verification of web services compositions with timed automata[J].Electronic Notes in Theroretical Computer Science,2006,157(2):19-34.[3] Cambronero M E,Diaz G,Valero V,et al.Validation and verification of web services choreographies by using timed automata[J].The Journal of Logic and Algebraic Programming,2011,80(1):25-49.[4] Salaum G,Bordeaux L,Schaerf M.Describing and reasoing on web services using process algebra [A].Proceeding of IEEE International Conference on Web Servce [C].Washinton:IEEE Computer Society,2004.43-51.[5] Peng Y,Ye L,Zheng Z,et al.Automatic service composition verification based on Pi-calculus [A].Proceeding of International Conference on E-Business and Information System Security [C].Wuhan:IEEE,2009.1-4.[6] Hinz S,Schmidt K,Stah C.Transforming BPEL to petri-nets[J].Lecture Notes in Computer Science,2005,3649:220-235.[7] Song W,Ma X.Ye,C,Dou W,Lu J.Timed modeling and verification of BPEL processed using timed Petri nets [A].Proceeding of the 9th International Conference on Quality Software [C].Cheju:IEEE,2009.92-97.[8] Package org.apache.ode.bpel.compiler.bom [CP/OL].http://www.jarvana.com/javana/view/or/apache/ode-bpel-compiler/1.3.4/ode-bpel-compiler-1.3.4-javadoc.jar!/org/apache/od.[9] 张功源.BPEL组合服务并发结构的分析与验证 [D].江苏南京:东南大学,2011.3. Zhang Gongyuan.Analysis and Verification of Concurrent Construct for BPEL-Based Service Composition [D].Nanjing,Jiangsu:Southeast University,2011,3.(in Chinese)[10] Amighi A.Flow Graph Extraction for Modular Verification of Java Programs [D].Stockholm:KTH Royal Institute of Technology,2011.[11] Kazhamiakin R,Pistore M.Static verification of control and data in web service compositions [A].Proceeding of IEEE International Conference on Web Services(ICWS'06) [C].Washington:IEEE Computer Society,2006.83-90.[12] Moser S,Martens A,et al.Advanced verification of distributed WS-BPEL business processes incorporating CSSA-based data flow analysis [A].IEEE International Conference on Service Computing [C].Salt Lake City:IEEE,2007.98-105.[13] Monakova G,Kopp O,et al.Verifying business rules using an SMT solver for BPEL processes [A].Proceedings of the Business Process and Services Computing Conference(BPSC'09) [C].Germany,2009.81-94.[14] Yang X,Huang J,Gong Y.Static data flow analysis and anomalies detection for BPEL [A].Proceeding of International Conference on Test and Measurement(ICTM) [C].Hong Kong:IEEE,2009.18-21.[15] Lei K,Zhang P.P,Lang B.Data access exception detecting of WS-BPEL process based on workflow nets [A].Proceding of International Conference on Computational Intelligence and Software Engineering(CiSE) [C].Wuhan:IEEE,2010.1-6.[16] Xu C,Qu W,Wang,H,etc.A Petri net-based method for data validation of web services composition [A].Proceeding of 34th International Computer Software and Applications Conference [C].Seoul:IEEE,2010.468-476.[17] 朱敏,李必信,等.基于微分动态逻辑的CPS建模和属性验证[J].电子学报,2012,40(6):1126-1132. Zhu Min,Li Bixin,et al.Transforming hybridUML to hybrid program for CPS property verification[J].Acta Electronica Sinica,2012,40(6):1126-1132.(in Chinese) |