CPC H04L 41/145 (2013.01) | 20 Claims |
1. A method, at a network device in a network, for verification of the network, the method comprising:
obtaining, at the network device, a device-specific input binary decision diagram (BDD) representing a device-specific input header space to query for a network property of interest;
calculating a device-specific output BDD representing a device-specific output header space, wherein the device-specific output BDD is calculated by applying a device-level BDD to the device-specific input BDD, the device-level BDD representing logical behavior of the network device for the network property of interest;
wherein the device-level BDD is obtained by:
collecting data about states and configurations of network entities in the network device;
modeling each network entity as a respective Boolean function and encoding the respective Boolean function as a respective entity-level BDD; and
logically combining the respective entity-level BDDs to obtain the device-level BDD;
storing the device-specific input BDD and the device-specific output BDD; and
comparing the device-specific output BDD and the device-specific input BDD, to verify the network property of interest at the network device.
|