On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators
Software Engineering
2020-10-14 v2
Abstract
A novel model-based approach to verify dynamic networks is proposed; the approach consists in formally describing the network topology and dynamic link parameters. A many sorted first order logic formula is constructed to check the model with respect to a set of properties. The network consistency is verified using an SMT-solver, and the formula is used for the run-time network verification when a given static network instance is implemented. The z3 solver is used for this purpose and corresponding preliminary experiments showcase the expressiveness and current limitations of the proposed approach.
Cite
@article{arxiv.2009.10051,
title = {On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators},
author = {Erick Petersen and Jorge López and Natalia Kushik and Claude Poletti and Djamal Zeghlache},
journal= {arXiv preprint arXiv:2009.10051},
year = {2020}
}
Comments
New version with experimental results submitted to NCA 2020 as a work in progress paper