Bounded Model Checking Web Services Composition via Verics
Sha Zong-lu · Journal of Chinese Computer Systems · 2011
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.