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.

Additional Metadata
Keywords DEVS simulation, Timed automata, Web search engines
Persistent URL dx.doi.org/10.22360/SummerSim.2016.SCSC.023
Conference 48th Summer Computer Simulation Conference, SCSC 2016, Part of the 2016 Summer Simulation Multi-Conference, SummerSim 2016
Alonso, I.-P. (Inostrosa-Psijas), Vcronica, G.-C. (Gil-Costa), Wainer, G.A, & Marin, M. (Mauricio). (2016). Formal verification of DEVS simulation: Web search engine model case study. In Simulation Series (pp. 124–131). doi:10.22360/SummerSim.2016.SCSC.023