摘要：
A clear trend within the context of computer networks is the use of software as an alternative to the use of specialized hardware. The benefit of this trend is an enhancement of flexibility, modularity, and maintainability of network components. Concurrently, it is challenging to de termine if everything is happening correctly in a computer network where software, possibly with bugs, is very present. To deal with this challenge, network testing is frequently used to check if a network component respects a given property and consequently performs its actions correctly. As there is a variety of causes for the abnormal operation of the network, ranging from human mistakes (inserting misconfiguration) to malicious activities, there are many chal lenges to network testing to achieve satisfactory results. Research in this field frequently tries to improve network testing by the use of formal verification techniques and network monitoring to detect property violations, such as configuration errors and policy conflicts. However, formal verification by itself cannot detect a property violation that was not anticipated and included in the model. Similarly, network monitoring needs to wait for a property violation to occur to de tect it. Consequently, both enhancement efforts fail to achieve a complete result. In this thesis, we investigate the problem of achieve the absence of property violations by combining the ad vantages of network monitoring for detecting property violations with the advantages of formal verification to model the network and prove the existence or absence of property violations. A highlight related to the success of such a combination is the use of a model based on grammars to capture the communication patterns existing on the network. Our analysis allows the eval uation of high-level properties such as "Can network component x send HTTP packets? " and the detection of property violations, such as conflicting forwarding rules, as soon they occurred in th
