PV2 ⊧ SyNETgenerates configurations for routers such that given requirements are satisfied

Synthesises network wide configurations given forwarding requirements.

Application domain/field

• Computer networks
• Network configuration

Type of tool

Synthesis tool for network configurations

Expected input

• Topology of the network
• Requirements
• Routing protocol

Format:

• Network topology: set of Datalog predicates, .logic file
• Requirements: .logic file
• Routing protocol: passed as an argument, the user can choose between static, ospf or bgp.

Expected output

Datalog input that results in a forwarding state satisfying the requirements. From this Datalog input one can derive the configurations for routers.

Internals

Uses Z3 to check whether the generated SMT constraints are satisfiable and to obtain a model.

Comments

License: Apache v2.0