Formal verification of a DEVS simulation model of a Storm application
Keywords:
Simulation, Formal verification, DEVS, Timed automatonAbstract
Stream processing platforms allow real-time data manipulation and analysis. A popular system for this purpose is the Storm platform, a scalable, fast, and fault-tolerant distributed computing system. Determining the appropriate number of processors to run Storm applications is challenging, especially for large-scale use. This paper presents a simulation model of a Storm application using the DEVS formalism, then defines an equivalent model using Timed Automata (TA). Through bisimulation, it is verified that both models are equivalent. Finally, the TA model is formally verified, proving that the simulation model behaves the same as the real application.
Downloads
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2024 Revista Ingeniare
This work is licensed under a Creative Commons Attribution 4.0 International License.
Authors retain copyright of their work and grant the journal the right of first publication under the Creative Commons CC-BY Attribution License, which permits unrestricted use, distribution, and reproduction provided the original authorship and the journal’s first publication are acknowledged.
