In this paper we introduce a specification model for the host migration
process in Software Defined Network, and for verifying the reachability
property for packets that do not change after the migration, and achieve
the required modifications to
meet the same properties.
The model is designed by TLA+ language and verified by TLC which is
correlated with it. The model is implemented by few states to meet the
required property.
In this paper the network specification by logic algebra is presented then
the packets are classified into reachable packets and dropped packets
according to the current state of the network and flow tables of switches.
The model specification is
written by TLA+ language which is built on
First Order Logic (FOL), and the specification is checked by TLC.
This model will help the programmers to detect the network in proactive
verification and prove that this configuration meets the global policy of
the network.
