期刊文献+

基于UML2.0序列图的Web服务运行时验证方法 被引量:3

Runtime Verification Method for Web Service Based on UML2.0 Sequence Diagrams
下载PDF
导出
摘要 为了确保包括非功能属性在内的服务规约与服务实际运行行为之间的一致性,提出一种Web服务运行时行为验证方法。首先对UML 2.0序列图进行扩展,将QoS属性和功能属性的描述统一起来,以精确表达Web服务的需求规约。然后,提出利用确定有限自动机构造出扩展序列图(Extended Sequence Diagrams,ESD)的语义模型的方法。最后,给出验证准则,根据Web服务的交互消息和规约建模的结果来验证Web服务运行时行为与需求规约之间的一致性。基于上述研究,设计开发了Web服务运行时验证工具(Runtime Verification Tool for Web Services,RVT4WS),以支持对Web服务运行时行为的验证。 To verify the consistency between run-time behavior of Web service and its specification, a runtime verifica- tion method for Web Service was proposed. In this paper, UML2.0 Sequence 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 con- sistency 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.
出处 《计算机科学》 CSCD 北大核心 2013年第7期138-142,共5页 Computer Science
基金 国家自然科学基金资助项目(61100017 61262089) 自治区高校科研计划项目(XJEDU2011S24) 福建省自然科学基金项目(2012J01250 2011J05146) 新疆大学博士毕业生科研启动基金项目(BS090142)资助
关键词 UML2 0序列图 确定有限自动机 WEB服务 运行时验证 UML2.0 sequence diagrams, Deterministic finite automata, Web service, Runtime verification
  • 相关文献

参考文献22

  • 1Christopher F, Joel F. What are Web services? [J]. Communi- eations of the ACM,2003,46(6):31.
  • 2Leucker M, Sehallhart C. A brief account of runtime verification [J]. The Journal of Logic and Algebraic Programming, 2009, 78 (5) : 293-303.
  • 3张岩,梅宏.UML类图中面向非功能属性的描述和检验[J].软件学报,2009,20(6):1457-1469. 被引量:16
  • 4Ran S. A Model for Web Services Discovery With QoS[J]. ACM Special Interest Group on Electronic Commerce, 2003,4 (1) : 1-10.
  • 5Hamilton K,Miles R. Learning UML2.0 [M]. O'Reilly Media,2006:179-222.
  • 6ITU-TS. Message Sequence Chart 1996, ITU-TS Recommenda- tion Z. 120[R]. Geneva,TU-TS, 1996.
  • 7Datum W, Harel D. LSCs:Breathiog Life into Message Sequence Charts[J]. Formal Methods in System Design, 2001,19 (1) : 45- 80.
  • 8David H, Shahar M. Assert and nagate Revisited:Modal seman- tics for UML sequence diagrams [J]. Software and Systems Modeling, 2008, ? (2) : 237-252.
  • 9Autili M, Inverardi P, Pelliecione P. A Scenario Based Notation for Specifying Temporal Propertiesl-A]ffProeeeding of the 2006 International workshop on Scenarios and state machines: mod- els, algorithms, and tools, 2008 [ C]. NewYork: ACM, 2006 21- 28.
  • 10Ameedeen M A, Bordbar B. A Model Driven Approach to Repre- sent Sequence Diagrams as Free Choice Petri Nets[A]//The 12th International IEEE Conference on Enterprise Distributed Object Computing, 2008[C]. NewYork: IEEE Computer Socie- ty,2008:213-221.

二级参考文献73

共引文献84

同被引文献22

引证文献3

二级引证文献2

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部