On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators
This work addresses network verification for dynamic systems, but it appears incremental as it builds on existing SMT-solver techniques without broad SOTA impact.
The authors tackled the problem of verifying dynamic networks by proposing a model-based approach that uses SMT-solvers to check network consistency and runtime properties, with preliminary experiments demonstrating expressiveness and limitations.
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.