Abstract Model Checking for Web Services  

作　　者：QIAN Junyan CAI Guoyong GU Tianlong ZHAO Lingzhong 

机构地区：[1]Department of Computer Science and Technology, Guilin University of Electronic Technology, Guilin 541004, Guangxi,China

出　　处：《Wuhan University Journal of Natural Sciences》2008年第4期466-470,共5页武汉大学学报（自然科学英文版）

基　　金：the National Natural Science Foundation of China (60663005, 60563005);the Natural Science Foundation of Guangxi Province (0542036, 0728093, 0728089)

摘　　要：Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.Web-services are highly distributed programs, and concurrent software is notoriously error-prone. Model checking is a powerful technique to find bugs in concurrent systems. However, the existing model checkers have no enough ability to support for the programming languages and communication mechanisms used for Web services. We propose to use Kripke structures as means of modeling Web service. This paper presents an automated way to extract formal models from programs implementing Web services using predicate abstraction for abstract model checking. The abstract models are checked by means of a model checker that implements automatic abstraction refinement. These results enable the verification of the applications that implement Web services.

关 键 词：Web-services model checking predicate abstraction hypertext preprocessor 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]