On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators

TL;DR

This paper presents a formal, SMT-based method for verifying dynamic network models by encoding network properties into logical formulas and using SMT-solvers like Z3 for runtime verification.

Contribution

It introduces a novel model-based approach that formalizes dynamic network verification using first-order logic and SMT-solvers, enabling effective runtime consistency checks.

Findings

The approach effectively verifies network consistency.

Preliminary experiments demonstrate the method's expressiveness.

Limitations of the current approach are identified.

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.