时间约束条件下web服务组合的形式化分析与验证

《时间约束条件下web服务组合的形式化分析与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、学校代码：10385分类号：研究生学号：1101401010密级：工程硕士专业学位论文时间约束条件下web服务组合的形式化分析与验证FormalAnalysisandVerificationofWebServiceCompositionswithTimingConstraints作者姓名：陈志辉指导教师：谭鸽伟(讲师)工程单位导师：工程领域：电子与通信工程研究方向：软件工程、服务计算所在学院：电子与通信工程论文提交日期：二〇一五年五月三十日摘要摘要随着Web技术和商业应用的快速发展，面向服务的计算(SOC

2、)和面向服务的体系结构(SOA)也已成为人们关注的焦点。由于两者的出现，有效解决在分布以及异构环境下软件集成与复用。当前，日益成熟的Web服务技术也为两者提供了有效地技术支撑。Web服务是一种基于网络的具有松耦合、独立性强等特点的软件构件。服务是Web体系中交互的基本单位。由于单个Web服务的功能有限，web服务组合技术已成构建电子商务应用的主要方法之一。然而，如何确保在复杂环境下的Web服务能够保证软件的质量，满足人们的预期呢？特别是限定服务的行为必须满足给定的时间约束条件。形式化技术作为软件质量保证的

3、一种重要方法。当前，为适应快速变化的商业环境，对商业应用提出了实时性的要求。即文中提出了一种形式化方法，用于分析与验证web服务组合的时间约束行为。首先，扩展了Web服务接口描述语言，增加对时间约束的描述，然后定义一种时间行为自动机，用于刻画web服务组合的时间行为，最终利用模型验证技术来自动验证这些行为是否满足给定的时间属性。通过对股票分析应用场景以及使用UPPAAL模型验证工具，表明该方法的可行性和有效性。深入研究服务组合建模与验证技术可以保障服务组合的可靠性。关键词：服务组合形式化方法时间自动机UP

4、PAAL模型检查I华侨大学硕士学位论文AbstractWiththerapiddevelopmentofWebtechnologyandthecommercialapplication,Service-OrientedComputing(SOC)andService-OrientedArchitecture(SOA)hasbecomethefocusofPeople’sattention.Asbothofthemappear,SOCandSOAsolvetheintegrationandreuseofso

5、ftwareproblemseffectivelyindistributedandheterogeneousenvironment.Atpresent,thematurechnologyofWebserviceincreasinglyprovidesthebesttechnicalsupportforSOCandSOA.Webserviceisasoftwarecomponentwhichisbasedonnetwork,andithasthecharacteristicsofloosecouplinga

6、ndstrongindependence.ServiceisthebasicInteractiveunitofWebsystem.AsindividualWebservicehasitslimitations,thetechnologyofwebservicecompositionhasbecomeoneofthemainmethodstoconstructtheelectroniccommerceapplication.However,howtoensurethatthecompositionsofth

7、eWebservicecanguaranteethequalityofsoftwareinthecomplexenvironmentandmeetpeople'sexpectations?EspeciallythelimitedservicebehaviormustsatisfytheconditiongiventimingConstraints.Theformaltechnologyprovidesanimportantmethodtoensurethequalityofsoftware.Inorder

8、toadapttothefast-changingbusinessenvironment,Peopleputsforwardtherequirementsofreal-timeforcommercialapplicationsatpresent.Inthispaper,wepresentaformalmethodforanalyzingandverifyingtime-relatedpropertiesofwebservice