通信学报
通信學報
통신학보
JOURNAL OF CHINA INSTITUTE OF COMMUNICATIONS
2012年
z1期
1-8
,共8页
张广泉%狄浩军%石慧娟%晏荣杰%朱雪阳
張廣泉%狄浩軍%石慧娟%晏榮傑%硃雪暘
장엄천%적호군%석혜연%안영걸%주설양
Web服务组合%定量属性%有限自动机%CTL%UPPAAL
Web服務組閤%定量屬性%有限自動機%CTL%UPPAAL
Web복무조합%정량속성%유한자동궤%CTL%UPPAAL
针对目前 Web服务组合研究中缺少对定量属性的验证以及在服务运行过程中缺乏对出现异常时的故障处理等问题,提出了一种基于扩展有限自动机的Web服务组合静态与动态验证方法.该方法首先对有限自动机进行扩展,建立了一个可以描述数据及时间等信息的Web服务组合形式化模型;基于该模型,采用计算树逻辑(CTL)描述相关属性,并利用模型检测工具UPPAAL对 Web服务组合的行为属性、时间属性以及数据属性等进行了验证;最后结合所建立的诊断模型,给出了一种能够对Web服务组合运行过程中出现异常时进行有效处理的错误诊断算法.
針對目前 Web服務組閤研究中缺少對定量屬性的驗證以及在服務運行過程中缺乏對齣現異常時的故障處理等問題,提齣瞭一種基于擴展有限自動機的Web服務組閤靜態與動態驗證方法.該方法首先對有限自動機進行擴展,建立瞭一箇可以描述數據及時間等信息的Web服務組閤形式化模型;基于該模型,採用計算樹邏輯(CTL)描述相關屬性,併利用模型檢測工具UPPAAL對 Web服務組閤的行為屬性、時間屬性以及數據屬性等進行瞭驗證;最後結閤所建立的診斷模型,給齣瞭一種能夠對Web服務組閤運行過程中齣現異常時進行有效處理的錯誤診斷算法.
침대목전 Web복무조합연구중결소대정량속성적험증이급재복무운행과정중결핍대출현이상시적고장처리등문제,제출료일충기우확전유한자동궤적Web복무조합정태여동태험증방법.해방법수선대유한자동궤진행확전,건립료일개가이묘술수거급시간등신식적Web복무조합형식화모형;기우해모형,채용계산수라집(CTL)묘술상관속성,병이용모형검측공구UPPAAL대 Web복무조합적행위속성、시간속성이급수거속성등진행료험증;최후결합소건립적진단모형,급출료일충능구대Web복무조합운행과정중출현이상시진행유효처리적착오진단산법.
