establishing a network model: using formal description language to specify the network model comprised of network components with complex configurations and relationships of the network components;

defining reachability semantics based on the network model: extracting a reachability of the network model and establishing a formal semantic model that specifies reachability of the network model in three scenarios including a reachability between two nodes, a set of all nodes that have access to a certain node and a set of all nodes that a certain node is capable of accessing;

modeling an abstract layer of a set-based solving algorithm: obtaining an abstract formal model of the set-based solving algorithm that transfers network reachability problem into set intersection/differentiation operations of packet headers;

solving the reachability of the network model: solving the reachability of the network model using the abstract formal model obtained in three scenarios, including, the reachability between two nodes, the set of all nodes that have access to a certain node and the set of all nodes that a certain node is capable of accessing;

proving an equivalence between a reachability result and the reachability semantics, wherein when the reachability result and the reachability semantics are not equivalent, modifying an abstract model until the reachability results obtained by the formal semantic model is the same as the abstract model;

when the reachability result and the reachability semantics are equivalent, modeling a set-based concrete solving algorithm, wherein the concrete solving algorithm is a refinement of the abstract model, and a concrete model is represented by more specified data structures and additional variables;

proving that the concrete model is the refinement of the abstract model, wherein when the concrete model is not the refinement of the abstract model, the concrete model is adjusted until the concrete model is the refinement of the abstract model;

when the concrete model is the refinement of the abstract model, deriving executable code in functional programming languages from the concrete model using code generation technique supported by Isabelle/higher-order logic (HOL) tool; and

obtaining a reliable and efficient solving algorithm: that is, performing logical equivalence transformation on the executable code using C++ programming language to develop the set-based solving algorithm, and solving the reachability of the network model with optimization in time complexity and space complexity.