vix.ing · top · new · best · stats · spec

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

2020/09/21 by Erick Petersen, Petersen, Erick, Jorge López +8
Computer Science · Decision Sciences · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Simulation Techniques and Applications #Software Engineering (cs.SE) #Software Testing and Debugging Techniques #Software-Defined Networks and 5G

paper · pdf · doi:10.48550/arxiv.2009.10051

openalex publication_date 2020/09/21 · openalex created_date 2022/10/01 · openalex updated_date 2026/07/28

Abstract

A novel model-based approach to verify dynamic networks is proposed; the\napproach consists in formally describing the network topology and dynamic link\nparameters. A many sorted first order logic formula is constructed to check the\nmodel with respect to a set of properties. The network consistency is verified\nusing an SMT-solver, and the formula is used for the run-time network\nverification when a given static network instance is implemented. The z3 solver\nis used for this purpose and corresponding preliminary experiments showcase the\nexpressiveness and current limitations of the proposed approach.\n

Related