published by Aِl-Baath University
in 2016
in
and research's language is
العربية
Download
Abstract in English
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.
References used
AL-SHAER, E, & AL-HAJ, S, 2010 - FlowChecker: Configuration Analysis and Verification of Federated OpenFlow Infrastructures. In Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration,ACM PP: 37–44
BALL, T, & BJØRNER, N, & GEMBER, A, & ITZHAKY, S, 2014 - VeriCon: Towards Verifying Controller Programs in Software-Defined Networks. ACM, PP. 1-12
BAIER, C, & KATOEN, J 2007 - Principles of Model Checking. The MIT Press Cambridge, Massachusetts, England, May. (992)P