论文标题
关于使用SMT造器进行建模和验证动态网络模拟器
On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators
论文作者
论文摘要
提出了一种基于模型的新型方法来验证动态网络。该方法包括正式描述网络拓扑和动态链接参数。构建了许多分类的一阶逻辑公式，以检查模型相对于一组属性。使用SMT溶剂验证网络一致性，并在实现给定的静态网络实例时将公式用于运行时网络验证。 Z3求解器用于此目的，相应的初步实验展示了所提出方法的表达和当前局限性。
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.
