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.