diff options
Diffstat (limited to 'docs/developer')
| -rw-r--r-- | docs/developer/design/images/verigraph.png | bin | 207401 -> 153762 bytes | |||
| -rw-r--r-- | docs/developer/design/verigraph.rst | 23 |
2 files changed, 12 insertions, 11 deletions
diff --git a/docs/developer/design/images/verigraph.png b/docs/developer/design/images/verigraph.png Binary files differindex dfcd586..617d2d5 100644 --- a/docs/developer/design/images/verigraph.png +++ b/docs/developer/design/images/verigraph.png diff --git a/docs/developer/design/verigraph.rst b/docs/developer/design/verigraph.rst index 1362e23..a2e1508 100644 --- a/docs/developer/design/verigraph.rst +++ b/docs/developer/design/verigraph.rst @@ -26,24 +26,25 @@ Architecture VeriGraph exploits two sub-modules: - **Z3**, the SMT solver developed by Microsoft -- **Neo4JManger**, a module that can store service graphs into a *Neo4J* graph-oriented database +- **Neo4J**, a Java-based graph-oriented database -Neo4JManager can also extract from a service graph all the VNF chains that are -relevant for checking the reachability properties of that graph. +The Neo4J database is used for service graph manipulation and to extract from a +service graph all the VNF chains that are relevant for checking the reachability +properties of that graph. How the tool works ------------------ VeriGraph accepts JSON service graph descriptions that include endpoints, VNF instances, logical directed links connecting them, and VNF configurations. -When VeriGraph receives a service graph and a reachability property to verify, it forwards the graph -to Neo4JManager and asks Neo4JManager to extract the chains that connect the nodes addressed by the -property to be checked. For each one of these chains, VeriGraph builds a set of first order logic -formulas that represent a mathematical model of the forwarding behavior of the chain. -This model takes into account the forwarding behavior of the links and of the VNFs included in the chain, -taking into consideration their configurations. If the formulas that make up the model are satisfiable, -this means that it is possible for a packet to traverse the chain from one end to the other. -VeriGraph passes this model to Z3 which checks its satisfiability. +When VeriGraph receives a service graph and a reachability property to verify, it saves the graph +into Neo4J and it extracts the chains that connect the nodes addressed by the property to be +checked. For each one of these chains, VeriGraph builds a set of first order logic formulas that +represent a mathematical model of the forwarding behavior of the chain. +This model takes into account the forwarding behavior of the links and of the VNFs included in the +chain, taking into consideration their configurations. If the formulas that make up the model are +satisfiable, this means that it is possible for a packet to traverse the chain from one end to the +other. VeriGraph passes this model to Z3 which checks its satisfiability. Based on the satisfiability result of the formulas that model the different paths, VeriGraph finally derives the overall result (reachability property satisfied or not). |
