Approach to Software-defined Network virtual topology checking

Abstract

At present, the concept of Software-defined Networks (SDN) is broadly considered to be among the defining technologies prompting further development of the Internet – as the Internet of Things (SDN). At the same time, taking into consideration the peculiarities of named networks, the concept of virtual topology is utilized. This allows react on the changes of the requirements to distributed software systems, built upon the network, in a flexible and agile manner. The problem of checking the consistency of resulting software solution arises here. With this statement in mind, the approach to checking the consistency of SDN-network virtual topology has been proposed. The proposed approach is grounded on the Temporal Logic of Actions (TLA) and corresponding TLA+ formalism usage. The approach is built over the concept of “action” – specification of transition between the states of transition system, defined by the TLA+ specification. To analytically represent the peculiarities of the proposed approach, the Kripke structure is used. The distinctive feature of the proposed approach is the flexibility – the formal model (specification) of the system can be operatively reconfigured with respect to the change of virtual topology of the network. To check the specification in an automated manner, the TLC (TLA Checker) implementation of model checking method is utilized. The implementation is based on traversing the states of transition system by way of Breadth-first Search (BFS).

Keywords: ad-hoc, Quality of Services, verification, virtual topology, Internet of Things, Model Checking, Software-defined Network, specification.