Name
Abstract | ||
|---|---|---|
Network Function Virtualization (NFV) architectures are emerging to increase networks flexibility. However, this renewed scenario poses new challenges, because virtualized networks, need to be carefully verified before being actually deployed in production environments in order to preserve network coherency (e.g., absence of forwarding loops, preservation of security on network traffic, etc.). Nowadays, model checking tools, SAT solvers, and Theorem Provers are available for formal verification of such properties in virtualized networks. Unfortunately, most of those verification tools accept input descriptions written in specification languages that are difficult to use for people not experienced in formal methods. Also, in order to enable the use of formal verification tools in real scenarios, vendors of Virtual Network Functions (VNFs) should provide abstract mathematical models of their functions, coded in the specific input languages of the verification tools. This process is error-prone, time-consuming, and often outside the VNF developers' expertise. This paper presents a framework that we designed for automatically extracting verification models starting from a Java based representation of a given VNF. It comprises a Java library of classes to define VNFs in a more developer-friendly way, and a tool to translate VNF definitions into formal verification models of different verification tools. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/COMPSAC.2017.16 | 2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC) |
Keywords | Field | DocType |
Formal verification,modeling,VNF,model extraction | Virtualization,Virtual network,Programming language,Model checking,Software engineering,Computer science,Formal methods,User Friendly,Java,Semantics,Formal verification | Conference |
Volume | ISSN | ISBN |
1 | 0730-3157 | 978-1-5386-0368-0 |
Citations | PageRank | References |
0 | 0.34 | 7 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Guido Marchetto | 1 | 86 | 20.64 |
| Riccardo Sisto | 2 | 556 | 56.79 |
| Matteo Virgilio | 3 | 31 | 2.91 |
| Jalolliddin Yusupov | 4 | 3 | 2.07 |