Formal Verification of DEVS Simulation: Web Search Engine Model Case Study
Alonso Inostrosa‐Psijas, Verónica Gil-Costa, Gabriel Wainer, Mauricio Marı́n · 2016
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.