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.
|Keywords||DEVS simulation, Timed automata, Web search engines|
|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