基于UML2．0序列图的Web服务运行时验证方法

计算机科学 ›› 2013, Vol. 40 ›› Issue (7): 138-138.

基于UML2．0序列图的Web服务运行时验证方法

张亚红,张琳琳,赵楷,陈佳丽,冯在文

新疆大学信息科学与工程学院乌鲁木齐830046;新疆大学信息科学与工程学院乌鲁木齐830046;新疆大学信息科学与工程学院乌鲁木齐830046;新疆大学信息科学与工程学院乌鲁木齐830046;武汉大学软件工程国家重点实验室武汉430072

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家自然科学基金资助

Runtime Verification Method for Web Service Based on UML2．0Sequence Diagrams

ZHANG Ya-hong,ZHANG Lin-lin,ZHAO Kai,CHEN Jia-li and FENG Zai-wen

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 为了确保包括非功能属性在内的服务规约与服务实际运行行为之间的一致性,提出一种Web服务运行时行为验证方法。首先对UML 2．0序列图进行扩展,将QoS属性和功能属性的描述统一起来,以精确表达Web服务的需求规约。然后,提出利用确定有限自动机构造出扩展序列图(Extended Sequence Diagrams,ESD)的语义模型的方法。最后,给出验证准则,根据Web服务的交互消息和规约建模的结果来验证Web服务运行时行为与需求规约之间的一致性。基于上述研究,设计开发了Web服务运行时验证工具(Runtime Verification Tool for Web Services,RVT4WS),以支持对Web服务运行时行为的验证。

关键词: UML 2．0序列图,确定有限自动机,Web服务,运行时验证中图法分类号TP311文献标识码A

Abstract: To verify the consistency between run-time behavior of Web service and its specification,a runtime verification method for Web Service was proposed．In this paper,UML2．0Sequence Diagrams were extended to describe the specification of Web service from both functional and QoS aspects,and then Extended Sequence Diagrams (ESD) were transformed to Deterministic Finite Automata to indicate semantics,and verification criteria was given to verify the consistency between run-time behavior and the specification．In addition,a runtime verification tool for Web service (RVT4WS) was developed to support the runtime verification method we proposed．

Key words: UML2．0sequence diagrams,Deterministic finite automata,Web service,Runtime verification

张亚红,张琳琳,赵楷,陈佳丽,冯在文. 基于UML2．0序列图的Web服务运行时验证方法[J]. 计算机科学, 2013, 40(7): 138-138. https://doi.org/

ZHANG Ya-hong,ZHANG Lin-lin,ZHAO Kai,CHEN Jia-li and FENG Zai-wen. Runtime Verification Method for Web Service Based on UML2．0Sequence Diagrams[J]. Computer Science, 2013, 40(7): 138-138. https://doi.org/

参考文献

[1] Christopher F,Joel F．What are Web services?[J]．Communi-cations of the ACM,2003,46(6):31
[2] Leucker M,Schallhart C．A brief account of runtime verification[J]．The Journal of Logic and Algebraic Programming,2009,78(5):293-303
[3] 张岩,梅宏．UML类图中面向非功能属性的描述和检验[J]．软件学报,2009,0(6):1457-1469
[4] Ran S．A Model for Web Services Discovery With QoS[J]．ACM Special Interest Group on Electronic Commerce,2003,4(1):1-10
[5] Hamilton K,Miles R．Learning UML2．0[M]．O’Reilly Media,2006:179-222
[6] ITU-TS．Message Sequence Chart 1996,ITU-TS Recommendation Z．120[R]．Geneva,TU-TS,1996
[7] Damm W,Harel D．LSCs:Breathing Life into Message Sequence Charts[J]．Formal Methods in System Design,2001,19(1):45-80
[8] David H,Shahar M．Assert and nagate Revisited:Modal semantics for UML sequence diagrams[J]．Software and Systems Modeling,2008,7(2):237-252
[9] Autili M,Inverardi P,Pelliccione P．A Scenario Based Notation for Specifying Temporal Properties[A]∥Proceeding of the 2006International workshop on Scenarios and state machines:models,algorithms,and tools,2006[C]．NewYork:ACM,2006:21-28
[10] Ameedeen M A,Bordbar B．A Model Driven Approach to Represent Sequence Diagrams as Free Choice Petri Nets[A]∥The 12th International IEEE Conference on Enterprise Distributed Object Computing,2008[C]．NewYork:IEEE Computer Society,2008:213-221
[11] Li X,Qiu X,Wang L,et al．UML Interaction Model-drivenRuntime Verification of Java Programs [J]．The Institution of Engineering and Technology,2011,5(2):142-156
[12] 雷丽晖,段振华．一种基于扩展有限自动机验证组合Web服务的方法[J]．软件学报,2007,8(12):2980-2990
[13] Jocelyn S,Yuan G,Marsha C,et al．Runtime Monitoring of Web Service Conversation[J]．IEEE Transaction on Services Computing,2009,2(3):223-244
[14] 苏焕成,黄志球,刘林源．基于接口自动机的BPEL4WS Web服务组合形式化模型[J]．计算机应用研究,2009,6(5):1774-1777
[15] 骆翔宇,轩爱成,沙宗鲁．基于时间自动机的Web服务模型检测[J]．计算机科学,2010,7(8):139-142
[16] 肖芳雄,李燕,黄志球,等．基于时间概率代价进程代数的Web服务组合建模和分析[J]．计算机学报,2012,5(5):918-935
[17] 朱俊,郭长国,吴泉源．基于CPN的服务交互行为关键属性的运行时确保机制[J]．电子学报,2011,9(5):1064-1071
[18] Walid G l,Sami B,Mohsen R．Event-based Design and Runtime Verification of Composite Service Transactional Behavior [J]．IEEE Transactions on Services Computing,2010,3(1)32-45
[19] 袁敏,黄志球,胡军．跨组织多业务事务建模与验证方法[J]．软件学报,2012,3(3):517-538
[20] Dimitris D,Ervin R,Dimitrios K．Runtime Verification of Behavioral Conformance for Conversational Web Services[A]∥The 7th IEEE European Conference on Web Services,2009[C]．NewYork:IEEE Computer Society,2009:139-147
[21] Andreas B,Martin L,Christian S．Runtime Verification for LTL and TLTL [J]．ACM Transactions on Software Engineering,2011,20(14):14-77
[22] 石慧娟,戎玫,张广泉,等．基于XYZ/ADL的异步Web服务组合描述与验证[J]．计算机科学,2011,38(12):139-143

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed