Formal verification of DEVS simulation: Web search engine model case study

Web search engines (WSE) are complex and highly optimized systems operating over large clusters of processors which manage high and dynamic and unpredictable user query bursts. The modeling, simulation and formal verification of shush systems is a challenge task which includes to manage user behavior and hardware costs. In this paper, we propose a WSE modeled with DEVS to be efficiently deployed on a distributed cluster of computers. The proposed model aims to reduce the communication overhead introduced by the message passage among the different hierarchical components of the DEVS model. This model is formally verified by using an equivalent Timed Automata model. © 2016 Society for Modeling & Simulation International (SCS).