Bounded Model Checking Web Services Composition via Verics
LUO Xiang-yu1,2, XUAN Ai-cheng3, SHA Zong-lu3
1(College of Comupter Science & Technology, Huaqiao University, Xiamen 361024,China),2(School of Software, Tsinghua University, Beijing 100084, China),3(School of Computer and Control, Guilin University of Electronic Technology, Guilin 541004, China)
Abstract：The traditional model checking techniques can not describe the epistemic logic for systems. However, for distributed systems, the multi-agent temporal epistemic logics are suitable to express the desired properties of systems and protocols. The Web services composition is a typical kind of distributed systems. In order to guarantee the correctness of Web services, we first regard a Web services composition as a multi-agent system and translate the system description into a network of timed automata. We then apply Verics, a model checker for timed and multi-agent systems, to the verification of the usability, reliability and time-efficiency of Web services compositions, via temporal epistemic logic. To illustrate the effectiveness of the proposed method, we model a particular case study of a travel reservation system and check the related properties.
骆翔宇1,2，轩爱成3，沙宗鲁3. 基于Verics的组合Web服务有界模型检测[J]. , 2011, 32(3): 412-415.
LUO Xiang-yu1,2, XUAN Ai-cheng3, SHA Zong-lu3. Bounded Model Checking Web Services Composition via Verics. , 2011, 32(3): 412-415.
