  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.
