published by Aِl-Baath University
in 2016
in
and research's language is
العربية
Download
Abstract in English
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.
References used
AL-SHAER,E., MARRERO,W., EL-ATAWY,E., ELBADAWI,K., 2009- Network configuration in a box: towards end-to-end verification of network reachability and security. ICNP-17th IEEE International Conference , PP:123– 132
CHURCHED, A, ZHOU, W, CAESAR, M. &GODFREY,P., 2012- “Overflow: Verifying network-wide invariants in real time,” ACM SIGCOMM Computer Communication Review, vol. 42, no. 4, PP:467–472
HP business white paper, 2013- prepare for software defined networking , build the foundation for SDN with OpenFlow. URL: hp.com/networking/openflow