Transcript here

Formal Verification of AODV Protocol
using cadence SMV
(CPSC513 Course Project)
Jun Wang and Xin Liu
[email protected], [email protected]
Outline
 Motivation
 AODV Introduction
 cadence SMV Introduction
 Building Model
 Conclusion
Motivation
 Find an appropriate approach to use cadence
SMV verifying real-life software communication
protocols, such as AODV. The emphasis is how
to build the model.
 Find some bugs in current AODV protocol
(RFC3561)? Hope we can…
AODV Introduction
Background



A mobile ad hoc network is a collection of nodes which
communicate over wireless channels. “ad hoc” means
that the nodes are free to move randomly.
need routing protocol


Proactive: table driven
Reactive: on demand
AODV (Ad hoc On-demand Distance Vector)
Protocol





a reactive routing protocol for ad hoc mobile networks.
3 control messages: RREQ, RREP, REER
Sequence number
Important property: Loop free
cadence SMV Introduction
 Find an appropriate approach to use cadence
SMV verifying real-life software communication
protocol, such as AODV. The emphasis is how to
build the model.
 Find some bugs in current AODV protocol
(RFC3561)? Hope we can…
Distributed Architecture
Distributed vs. Centralized
 Distributed
 Robustness: failure of any participant has no effect on
other participants.
 Scalability: while in centralized architecture, server is the
bottleneck.
 Minimum delay: information crosses the network only
once to reach its final destination, while in centralized
architecture, information reaches its destination through the
server.
 Centralized
 Consistency: Global consistency is guaranteed.
 Cheating difficult: the presence of server makes
cheating difficult.
 Easily charge: allow game companies to easily charge
Distributed Architecture (cont.)
 MiMaze Architecture:
Note: the game server is only used when a new entity joins a session, to
learn the session group and to download the game.
Distributed Architecture (cont.)
 Fully distributed, Serverless architecture.
 Based on RTP/UDP/IP multicast.
 Only one multicast group in MiMaze.
 Game server is only used when new
participant joining the game session.
 Once the game has started, participants
exchange their own states (including position,
direction, speed,…) to compute the game
state.
 In MiMaze, no central entity (or server) exists
to compute the game state, each participant
computes its own view of the game state
(may be inconsistent).
Bucket Synchronization Mechanism
 Distributed synchronization


All ADUs issued at the same time are computed together
to evaluate the state of the game.
All the session entities display the same game state
simultaneously.
 MiMaze bucket synchromization




Time is divided into fixed length periods and a bucket is
associated with each period.
All ADUs received by a player are stored in the bucket
corresponding to the time interval in which senders issue
the ADUs.
At the end of every bucket interval, all ADUs in that bucket
are used by the entity to compute its local view of the
global game state.
Bucket will be computed 100ms after the end of the
sampling period during which ADUs have been issued,
which is the playout delay.
Bucket Synchronization
Mechanism
 Bucket frequency
 The bucket frequency defines the rate at
which a new game state is computed and
displayed.
 In MiMaze, the bucket frequency is 25
buckets per second.
 The ADU transmission frequency is equal to
the bucket frequency, thus, there should be
one new ADU per entity at the time a bucket
is processed.
Bucket Synchronization Mechanism
 Example:
Bucket Synchronization
Mechanism
 Global clock mechanism
 The bucket synchronization mechanism uses
NTP to evaluate the delay between
participating entities.
 If NTP is not available, use a NTP-like
algorithm based on the evaluation of the round
trip time.
 There are 3 levels (strata) of NTP servers and
it is very difficult to maintain good
synchronization when level 3 servers are
involved.
 In order to increase the precision of NTP under
stratum 2 and 3, use both NTP and NTP-like
algorithm.
Dead reckoning
 What is dead reckoning?
 Dead reckoning is an extrapolation
techniques used in the aviation systems to
compute an estimate of the current
position of a plane based on the knowledge
of its position in the past and on its
trajectory.
 An important property of game objects’
behavior:
 “Continuous”, which means that the
behavior of avatar X at time t+1 can be
extrapolated from its behavior at time t
with high possibility.
Dead reckoning (cont.)
 Why need dead reckoning?
 To deliver a complete view of the game, the
bucket algorithm requires at least one ADU per
participant to be available in each bucket.
However, a ADU can be missing or late
(received after 100ms).
 MiMaze uses the simplest dead reckoning
algorithm
 When an avatar position (ADU) is missing at
the time we compute a bucket, simply replay
the last known position of this avatar.
 The late ADUs are still stored in their
destination bucket, since they are useful to
replace a missing ADU when computing future
buckets.
Dead reckoning (cont.)
 Error Control:

replace lost ADUs.
 Synchronization:

extrapolate late ADUs.
 Trajectory smoothing:

interpolation between received states when sender
frequency is lower than display frequency.
 Anticipating collisions:

dead reckoning can be used by the sending entities
to anticipate potential future collisions.
 Congestion control:

adapt ADU transmission frequency according to
network load.
Performance evaluation
 Experimental environment:



The evaluation of MiMaze is performed on the MBone with up
to 25 players located in various places in France.
The number of participants are varied in order to vary the
loss rate.
The architecture of the experimental multicast tree:
Performance evaluation (cont.)
 Monitoring
During the experiment, participants play MiMaze and
collect traces which is composed of:

Network level data: for each received ADU, collect
the senders’ identity, the transmission and reception
time-stamp, etc.

Application level data: information contained in all
ADUs sent and received is time-stamped and collected
in the trace file, which is used to reconstruct the state
of game computed by each participant.

Synchronization data: network delays and clock
offsets with respect to each participant are collected.
These data is used to resynchronize the traces.
Performance evaluation (cont.)
 Resynchronize traces
(main difficulty in analysis)
 Since the system is distributed, there is
no absolute clock in a game session, each
participant timestamps its local traces.
 Global clock mechanism is imperfect, use
an algorithm based on least-squares to
resynchronize traces.
 Omit time intervals where relative clock
information is not interpretable.
Performance evaluation (cont.)
 Distributed game metrics

Need a meaningful performance metric to analyze
distributed multiplayer games.

This metric should reflect how far the distributed
game behavior is from the perfect behavior if
without the network delay and lost.

Use “drift distance”. The drift distance represents
the distance units between the real position of an
avatar in local entity, and the position of the same
avatar computed by a remote entity.

The game is consistent if the drift distance is zero,
however, a small drift does not means that the game
is inconsistent.
Performance evaluation (cont.)

In order to keep figures clear, the paper present
performance observed between only two participants
(droopy and hugo).

Delay distribution: (between hosts hugo and droopy)
Performance evaluation (cont.)
 Percentage of late ADUs:
Note: between hosts hugo and droopy.
 Distribution of late
ADUs:
Note: between hosts hugo and droopy.
Performance evaluation (cont.)
 Percentage of lost ADUs:
Note: between hosts hugo and droopy.
 Distribution of lost
ADUs:
Note: between hosts hugo and droopy.
Performance evaluation (cont.)
 Drift distance:
Note: between hosts hugo and droopy.
 Distribution of drift
distance:
Note: between hosts hugo and droopy.
Performance evaluation (cont.)
 Consistency improvement (gain) with distributed
synchronization:
Note: a value 1 on the vertical axis corresponds to no gain and 2 corresponds to a 100% gain.
Summary
 MiMaze is implemented on a completely
distributed communication architecture based on
the IP multicast protocol suit (RTP/UDP/IP
multicast).
 MiMaze use a simple distributed synchronization
mechanism - the bucket mechanism to provide an
acceptable level of game state consistency.
 MiMaze shows that real-time interactive can be
maintained in the fully distributed applications,
provided that some level of inconsistency can be
tolerated by the applications.
Discuss
 Main Contribution:
 This work shows that with a multicast
communication architecture and with a simple
synchronization mechanism (the bucket
mechanism), a fully distributed interactive
application can provide an acceptable level of
consistency.
 It also identified the problem of defining a
proper metric for the evaluation of the
application consistency.
 This work is a proof of feasibility of distributed
multiplayer architectures on heterogeneous
best-effort networks (Internet).
Discuss (cont.)
 Related Work:
 Amaze:
can be considered as MiMaze’s ancestor. It is played on a
LAN, using point-to-point communication. Amaze transmits
the game state on the network, and maintains replicated
copies of the game state.
 Spline:
a virtual distributed interactive world. It has a distributed
architecture based on the DIS standard. Most of the efforts
has been done on local flow synchronization mechanism.
 PARADISE:
aims to architect and build a large-scale internet worked
simulation environment that supports multiplayer interactive
applications. It aims primarily at aggregation and specific
dead reckoning algorithms.
Discuss (cont.)
 Future Work:
 Extensions of MiMaze (has done)
 Using Synchronized 3D Virtual Reality
Modeling Language (VRML) to get a 3D
game.
 Mapping MPEG video on the maze wall.
 Supports 3D spatial audio.
 Congestion control
 Avatar collision detection and anticipation
 Session management in subgroups of
participants.
References






MiMaze http://www-sop.inria.fr/rodeo/MiMaze/
Design and Evaluation of MiMaze, a Multi-player Game on
the Internet, Laurent Gautier, Christophe Diot, IEEE
Multimedia Systems Conference, Austin, June 28 - July 1,
1998.
Distributed Synchronization for Multiplayer Interactive
Applications on the Internet, Laurent Gautier, Christophe
Diot, IEEE ICNP Conference, Austin, October 1998.
MiMaze, a 3D Multi-Player Game on the Internet , Emmanuel
Lety, Laurent Gautier, Christophe Diot, In the Proceedings of
the 4th International Conference on Virtual System and
MultiMedia, Nov 98, Gifu, Japan.
IEEE Standard for Distributed Interactive Simulation -Application Protocols (IEEE Std 1278.1-1995). IEEE
Computer Society. 1995.
S. Deering. "Host Extensions for IP Multicasting". RFC 1112.
17. August 1989.
A Distributed Architecture for Multiplayer Interactive
Applications on the Internet
Thanks!