Do you want to publish a course? Click here

According to the large number of the access rules that define the networks, and the dynamic changing of the network topology, that is the verification by hand of the important properties in the network such as reachability, access rules conflict fr ee and loop free is so hard to accomplish by the programmer. Formal specification of systems and protocols is considered one of the most important methods that is used to eliminate the ambiguous of the system configurations and find bugs of its work. A lot of the researches have been introduced in packet reachability and network specification domain, but a little of them are checked and analyzed by model checkers which help to detect the errors of these models. In this paper an abstraction model for dynamic networks specification has been introduced and developed to be appropriate for several important properties of the network such as reachability, no conflict..etc, depending on the network state. The proposed model specification is implemented by TLA+(Temporal Logic of Action) language which is a high level specification language built on Set-theory and First Order Logic, the model has been analyzed and the properties are checked by TLC model checking tool which used by TLA tool. Results show the correctness of the model, and improvement in reducing the response time and the required states to get the result of the verification.
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.
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا