一种面向Web服务源程序的谓词抽象验证方法  

An Predicate Abstraction Verification Method for Source Program of the Web Service

作　　者：任强[1] 张广泉[1,2] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006 [2]中国科学院软件研究所计算机科学国家重点实验室,北京100080

出　　处：《苏州大学学报（工科版）》2011年第2期14-19,共6页Journal of Soochow University Engineering Science Edition (Bimonthly)

基　　金：中国科学院计算机科学国家重点实验室开放课题(编号SYSKF0908);江苏省高校自然科学研究项目(编号08KJB520010)

摘　　要：Web服务作为一种典型的分布式计算技术,常用于跨平台跨组织的分布式环境,因此保证其安全性就显得十分重要。作为一种形式化验证方法,模型检测可以验证并发与分布式系统的安全性。现有形式化方法的验证对象多为Web服务高层描述语言,而针对Web服务底层执行程序的验证工作则较少。提出一种面向Web服务源程序的验证方法,采用谓词抽象技术,将源程序转化为抽象模型,最后通过实验说明此方法的可行性。As a kind of typical distributed computing technology,Web services is commonly used in cross-platform distributed environment,thus ensuring their safety becomes very important.As a method of formal verification,model checking can be used to verify the security of concurrent and distributed systems.The verification objects of existing formal methods are mostly the high-level Web service description languages,and the verification for underlying execution programs is less.We present a verification method for the source program of Web service by using predicate Abstraction technology,and transform the source program into Abstract model.And finally,the experimental results show the feasibility of this method.

关 键 词：WEB服务 模型检测 谓词抽象 源程序 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]