On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators: (Work in Progress)

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

In this paper, a novel model-based approach to verify dynamic networks is proposed. The network topology and dynamic link parameters are described as a many sorted first order logic formula, that is verified by an SMT-solver (z3 in our case) with respect to a set of properties. The formula is also used for run-time network verification when a given static network instance is implemented. Preliminary experiments showcase the expressiveness and current limitations of the proposed approach.

Original languageEnglish
Title of host publication2020 IEEE 19th International Symposium on Network Computing and Applications, NCA 2020
EditorsAris Gkoulalas-Divanis, Mirco Marchetti, Dimiter R. Avresky
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781728183268
DOIs
Publication statusPublished - 24 Nov 2020
Event19th IEEE International Symposium on Network Computing and Applications, NCA 2020 - Cambridge, United States
Duration: 24 Nov 202027 Nov 2020

Publication series

Name2020 IEEE 19th International Symposium on Network Computing and Applications, NCA 2020

Conference

Conference19th IEEE International Symposium on Network Computing and Applications, NCA 2020
Country/TerritoryUnited States
CityCambridge
Period24/11/2027/11/20

Keywords

  • Many sorted first order logic formula
  • Modeling
  • Network emulator
  • SMT-solver
  • Verification

Fingerprint

Dive into the research topics of 'On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators: (Work in Progress)'. Together they form a unique fingerprint.

Cite this