# US 11,121,934 B1 · Network verification systems and methods > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 11,121,934 B1 - Document ID: US11121934B1 - Status: Granted - Kind: B1 - Application number: 17/115,379 - Filed: 2020-12-08 - Granted: 2021-09-14 - Earliest claimed: 2020-07-23 - Assignees: Microsoft Technology Licensing, LLC - Applicants: Microsoft Technology Licensing, LLC - Inventors: Ryan Andrew Beckett; Karthick Jayaraman; Neha Milind Raje; Jitendra Padhye; Christopher Scott Johnston; Steven Jeffrey Benaloh; Nikolaj Bjorner; Andrey Aleksandrovic Rybalchenko; Nuno Cerqueira Afonso; Nuno Claudino Pereira Lopes; Sharad Agarwal; Hang Kwong Lee; Aniruddha Parkhi; Maik Riechert - Web page: https://patentgrep.com/patent/US11121934B1 ## CPC - H04L 41/0873: Checking configuration conflicts between network elements - H04L 41/0813: characterised by the conditions triggering a change of settings - H04L 41/145: {involving simulating, designing, planning or modelling of a network} - H04L 43/06: Generation of reports - H04L 43/50: Testing arrangements - H04L: TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION (arrangements common to telegraphic and telephonic communication H04M) ## Abstract A network verification system uses general-purpose programming language to create network verification tests. A test orchestrator builds a model of the network only using data from the network verification test. An optimization testing manager creates symbolic packets for verification tests using assertions based on a packet library embedded into the testing manager and the general-purpose programming language. ## Claims ### Claim 1 A method for verifying a change to a network, comprising: receiving a network change to be implemented on the network, the network change affecting transfer of data packets through the network; receiving a network verification test including test parameters, the test parameters including one or more invariants, wherein the one or more invariants include a condition for the transfer of the data packets through the network, and wherein the network verification test tests the transfer of the data packets and identifies network elements used by the data packets affected by the network change; retrieving network data from the network elements identified by the test parameters; building a representation of the network from the network data on which to run the network verification test, the representation of the network including representations of the network elements identified by the test parameters, the representation of the network being configured to transfer simulated data packets across the network elements; and applying the network verification test to the representation of the network data to determine whether the condition included in the one or more invariants is satisfied. ### Claim 2 (depends on 1) The method of claim 1, wherein the network data includes at least one of network topology, device metadata, IP addressing information, routing tables, or device configurations. ### Claim 3 (depends on 2) The method of claim 2, wherein applying the network verification test includes testing at least one element of the network data. ### Claim 4 (depends on 1) The method of claim 1, wherein building the representation of the network includes building the representation of the network only from the network data. ### Claim 5 (depends on 1) The method of claim 1, wherein the network verification test is written in a general-purpose programming language. ### Claim 6 (depends on 1) The method of claim 1, wherein the network verification test is separate from the representation of the network. ### Claim 7 (depends on 1) The method of claim 1, further comprising preparing a test report including results of the network verification test. ### Claim 8 (depends on 7) The method of claim 7, wherein the test report includes results from each element of the network verification test. ### Claim 9 (depends on 1) The method of claim 1, wherein receiving the network verification test includes identifying the test parameters from the network verification test. ### Claim 10 (depends on 1) The method of claim 1, wherein building the representation of the network includes generating a network graph of the network. ### Claim 11 A method for verifying a change to a network, comprising: receiving a network change to be implemented on the network, the network change affecting transfer of data packets through the network; receiving a network verification test; identifying test parameters from the network verification test, the test parameters including one or more invariants, wherein the one or more invariants include a condition for the transfer of the data packets through the network, and wherein the network verification test tests the transfer of the data packets and identifies network elements used by the data packets affected by the network change; generating a symbolic packet using an equivalence class for a plurality of data packets, the equivalence class correlating the plurality of data packets based on a similar data packet trait used to test the condition of the one or more invariants; and applying the network verification test on a representation of the network generated using the identified network elements using the symbolic packet. ### Claim 12 (depends on 11) The method of claim 11, further comprising identifying a packet assertion of a packet type in the network verification test, and wherein generating the symbolic packet includes evaluating the packet assertion based on a packet library of symbolic data types. ### Claim 13 (depends on 12) The method of claim 12, wherein generating the symbolic packet includes: creating an abstract syntax tree based on the packet assertion; and analyzing the abstract syntax tree with a binary decision diagram. ### Claim 14 (depends on 12) The method of claim 12, wherein generating the symbolic packet further includes generating a network graph based on the packet assertion. ### Claim 15 (depends on 11) The method of claim 11, further comprising: identifying a test assertion in the network verification test; and applying the test assertion to the symbolic packet. ### Claim 16 A network verification system, comprising: one or more processors; memory in electronic communication with the one or more processors; instructions stored in the memory, the instructions being executable by the one or more processors to: receive a network change to be implemented on a network, the network change affecting transfer of data packets through the network; receive a network verification test; identify test parameters from the network verification test, the test parameters including one or more invariants, wherein the one or more invariants include a condition for the transfer of data packets through the network, and wherein the network verification test tests the transfer of data packets and identifies network elements used by the data packets affected by the network change; retrieve network data from the network elements identified by the test parameters; build a representation of the network from the network data on which to run the network verification test, the representation of the network including representations of the network elements identified by the test parameters, the representation of the network being configured to transfer simulated data packets across the network elements; generate a symbolic packet using an equivalence class for a plurality of data packets, the equivalence class correlating the plurality of data packets based on a similar data packet trait used to test the condition of the one or more invariants; and apply the network verification test to the symbolic packet to determine whether the condition included in the one or more invariants is satisfied. ### Claim 17 (depends on 16) The system of claim 16, wherein the network verification test is written in a general-purpose programming language. ### Claim 18 (depends on 16) The system of claim 16, wherein the network verification test is separate from the representation of the network. ### Claim 19 (depends on 16) The system of claim 16, wherein generating the symbolic packet includes: creating an abstract syntax tree based on a packet assertion in the network verification test; and analyzing the abstract syntax tree with a binary decision diagram. ### Claim 20 (depends on 16) The system of claim 16, wherein generating the symbolic packet includes: creating an abstract syntax tree based on a packet assertion in the network verification test; and analyzing the abstract syntax tree with a binary decision diagram.