摘要: Web交互模型的形式化验证是对Web事件属性进行校验的十分可信的方法。通过一系列的系统模型建立、系统行为分析以及对于模型中关心属性的相关验证,能够让交互模型在设计阶段就能使形式化模型暴露出其所存在的缺陷,而不至于让缺陷保留到编码阶段或者更后面才能被真正地暴露出来,这样使系统模型的生存能力更加强大,同时避免了因后期缺陷暴露而出现的大代价修复。通过对Web系统的交互应用服务的过程模型化的体系进行研究,通过模型本身具有的属性进行相关正确性的校验,主要通过使用数学推理实现系统逻辑上的服务交互进程,从而进行过程的推演,并对系统服务的正确性进行过程的形式化验证,从而使系统服务模块的属性正确性可以通过逻辑上的演进来发现服务问题的存在,而不再是系统通过编码实现后才发现。对Web交互模型的形式化验证是基于IMWSC模型语义形成的IMWSC模型的验证机制。
[1] Misra J,Cook W.Computing Orchestration:A Basis for Wide-Area Computing[J].Journal of Software & Systems Modeling,2011,6(1):83-110 [2] Foster H,Uchitel S,Magee J,et al.LTSA-WS:A Tool for Mo-del-based Verification of Web Service Compositions and Choreo-graphy[C]∥Proc.of ICSE.2010:771-774 [3] George Z,B A.Service Mining on the Web[J].the VLDB Journal,2009,2(1):65-78 [4] Tsesmetzis D T,Russaki I,Papaioannou I V,et al.A QoS Ontology Language for Web Services[C]∥AINA.2009(1):101-106 [5] Bao Li,Zhang Wei-shi,Xie Xiong.A Formal Model for Abstracting the Interaction of Web Services[J].Journal of Computers,2010,5(1):91-98 [6] Bao Li,Zhang Wei-shi,Xie Xiong.Abstracting the Interaction of Web Services Using IMWSC[J].Journal of Information and Computational Science,2009,6(2):699-708 [7] Zhang Xiu-guo,Zhang Wei-shi.A Cooperative Service Composition Language and Its Formal Semantics[C]∥Proc.of the 7th International Conference on Parallel and Distributed Computing,Applications and Technologies (PDCAT 2008).TaiPei:IEEE Computer Society Press,2008 [8] Bemmel J V,Wegdam M,Lagerberg K.3PAC:Enforcing AccessPolicies for WebServices[C]∥IEEE International Conference on Web Services(ICWS’05).2005:589-596 [9] ter Beek M H,Bucchiarone A,Gnesi S.Formal Methods forService Composition[R].Technical Report.Software/Program Verification,Formal Methods,ACM [10] Endrei M,Ang J,Arsanjani A,et al.Patterns:service-Oriented Architecture and Web Services .http://www.redbooks.ibm.eom/redbooks/Pdfs/sg246303.pdf [11] 杨艺,周元.基于用户查询意图识别的Web搜索优化模型[J].计算机科学,2012,39(1):264-267 |
No related articles found! |
|