Specification of Synchronous Network
Flooding in Temporal Logic
Ra’ed
Bani Abdelrahman1, Rafat Alshorman2, Walter Hussak3,
and Amitabh Trehan3
1SoftwareEngineering
Department, Ajloun National University, Jordan
2Department
of Computer Science, Yarmouk University, Jordan
3Computer
Science Department, Loughborough University, United Kindom
Abstract:
In distributed network algorithms, network
flooding is considered one of the simplest and most fundamental algorithms. This
research specifies the basic synchronous memory-less network flooding algorithm
where nodes on the network don’t have memory, for any fixed size of network, in
Linear Temporal Logic. The specification can be customized to any single
network topology or class of topologies. A specification of the termination
problem is formulated and used to compare different topologies for earlier
termination. This paper gives a worked example of one topology resulting in
earlier termination than another, for which we perform a formal verification
using the model checker NuSMV.
Keywords:
Network flooding, linear temporal logic, model
checking.
Received December 17, 2018; accepted June 11,
2019