Dies ist eine alte Version des Dokuments!
Applying Formal Methods for QoS
Provisioning in Mobile Architectures
This project
focuses on the application of formal methods to model and manage QoS for
Network Mobility. The field of network mobility is gaining ground in
telecommunications because of the evolution of broadband technologies and the
increasing applications that demand broadband access, e.g. connectivity in
public transportation and IMS. Network Mobility is the field that considers
sets of mobile devices moving together as one entity with one or more access
points which are called mobile routers. These networks are standardized under
the IETF-RFC3963 specification also known as NEMO Basic Support, while QoS
challenges are described in IETF-RFC4980. NEMO BS is an extension to MIPv6
described under IETF-RFC3775. Mobile routers can possess multiple Radio
Access Technologies (RATs) and have to perform real-time operations, e.g.
handover, managing binding updates, merging/splitting mobile networks and
managing QoS. The intelligent management of mobility, data streams of
different QoS requirements and the available RATs makes the formalization of
this problem a necessity due to its complexity. The importance of this study
comes from the industry focus on network operator’s IP services, especially
IMS. NEMO BS provides a solution for this system and at the same time
requires investment in research to improve QoS. |
||
Work Plan
This
work consists of two main parts; building the formal model and simulating the
NEMO protocol. These parts are to be run in parallel to achieve
interdependability. This means that simulation measurements will be used to
support theoretic hypothesis made by the formalized description of the QoS
problem. On the other hand, formal tools have to be implemented in order
to be able to incorporate extensions which in turn will allow making
predictions of the behavior of the modeled system in a similar way to
simulations. This means that these tools will be designed to be able to
generate quantitative as well as qualitative conclusions. |
||
The Formal
Model
πCalculus |
||
Π-Calculus
is a modeling formality that focuses on communicating processes. It offers
firm representation of connectivity and messaging using math-like
expressions. Π-Calculus had initially a monadic syntax where single
arguments are passed through channels. Later on, polyadic π-Calculus was
introduced to allow pushing sets of arguments at once over the communication
channels. Process replication was also introduced. In the higher order
π-Calculus, process names can be exchanged through the channels too.
Some research uses available syntax to express problems like QoS while others
ground their own flavor of it by introducing modifications to the syntax like
spi-Calculus which is specifically suitable for cryptology. One more example
is Ambient-Calculus which concerns itself with defining computation domains
or ambiences where communication between local processes happens within its
boundary, ambiences can move and communication crossing the border is
analogous to crossing firewalls. The extensibility, expressiveness,
flexibility and firm formality of π-Calculus make it the most suitable
tool for modeling communication protocols and prototypes of enhancements.
This work aims to make further contributions to π-Calculus in order to
achieve the following: ·
Π-Calculus is
founded on the principle of state automata. Consequently, processes in
π-Calculus interact and switch their states upon reception of messages
over communication channels, which means that message reception among
processes triggers the interaction and causes the system to evolve. However,
modeling real-world systems needs more than that. The notion of time is
currently unavailable in the syntax of π-Calculus, which makes it
unsuitable for performing simulations in which particular events take place
at certain points of time, e.g. time-out events. In this work we aim to
introduce a new component in the syntax of π-Calculus to enable it to
model timed events. ·
Π-Calculus is
suitable for deducing qualitative conclusions about processes’ interaction
and states. However, more meaningful verification results can be made when
quantitative conclusions are made from the π-Calculus model such as
bandwidth utilization and power consumption. This can be done if the notion
of time was present in the model. Available tools for π-Calculus have
limitations to be covered, e.g. polyadic π-Calculus has to be supported
in order to be able to model process replication. Otherwise, polyadic systems
have to be downgraded to monadic syntax which is unrealistic for complex
systems. ·
There have been
models suggested about using π-Calculus to model QoS supervision in
telecommunication networks. As our work touches the foundations of
π-Calculus, we would like to see how these changes will affect the
suggested models and how we can improve them. ·
A π-Calculus
model for NEMO BS has to be built as described in RFC3963. Software
development of the protocol under the simulation tool and QoS enhancements
should be based on this model. This is important to ensure strong analogy
interrelationships between simulation measurements and the qualitative
deductions made from the formal model.
·
Depending on the
interdependency between simulation and formal model verification results
further studies can evolve to explain observed phenomena and try to set rules
to make this relation deterministic. The
ability to make realistic assessments of modeled systems before the
implementation phase using formal model checking techniques has several
advantages: ·
It will be possible
on basis of the qualitative attributes of the suggested model to judge
whether it answers the requirements it is meant to satisfy. ·
It allows
quantitatively comparing formal models and making early choices about
modifications and improvements. ·
It shortens the
software development cycle by limiting the need to go back to the model and
make modifications for issues discovered after implementation. |
||
Simulating
the Protocol
|
||
For this
purpose OPNET Modeler® is being used under university licensing. This
simulator contains a huge library of standardized protocols and devices as
well as commercial ones, e.g. MIPv6 and mobile routers. The hierarchical
structure of components and their modular design shortens the time required
to develop own devices and extend particular protocols. To complete the
required infrastructure for performing simulations the following tasks are
ahead: |
||
|
||
·
Create a multi-RAT
router on which the NEMO BS protocol is going to be run. Multiple RAT
interfaces are necessary to study the effect of access technology switching
on ongoing data sessions and to test possible QoS enhancements and
strategies. This router shares its network layer between the different RATs
by setting MIPv6 on top of Link Layer (LL) and Radio Resource Control (RRC)
layers of available RATs. Each RAT will have its own physical, MAC, LL, Radio
Link Control (RLC) and RRC of its own. On top of MIPv6 NEMO BS is going to be
implemented. This structure allows for unified session management and QoS
control. For this research, WiFi, WiMAX and UMTS are going to be the RATs of
our mobile routers. ·
Create core-network
components that will provide the required messaging to perform handover and
domain administration. These components are described in 3GPP-23.401 and
3GPP-23.402. These specifications describe network structure for different
scenarios (homing or visiting) in addition to mobility management, network
selection, network access strategies and QoS provisioning. ·
NEMO BS has to be
modeled using our extensions of π-Calculus. Afterwards, the protocol can
be implemented for simulation based on the prototyped model. This has to be
done in this order because strong interdependency between simulation and
formalization is required for further study purposes. ·
Extend MIPv6 to
include NEMO BS as described in RFC3963 and according to the prototyped
π-Calculus model. To allow code-reuse NEMO BS will be written above an
abstraction layer that will integrate it with OPNET. ·
Integrate the NEMO
BS extension with OPNET. At this point, full functionality of NEMO BS should
be available for testing. ·
Create test
scenarios for use with simulations. These scenarios will be based on the use
cases described in 3GPP-22.259. This document describes use-cases for PANs in
IMS for which NEMO BS represents a suitable solution. This particular
approach has been chosen in order to keep a close to industry requirements. ·
Collect baseline
measurements against which QoS improvements are going to be evaluated. ·
Modify the
implementation of NEMO BS to propagate the QoS improvements made using the π-Calculus
based model and collect simulation measurements. These measurements will be
compared with the baseline results to assess the improvements. In addition,
they will be semantically compared to the quantitative attributes of the QoS
improved model to see how these results match or differ. |
||
Contact
|
||
Kamal Barakat |
Tel. +49 (241) 80 21171 Fax +49 (241) 80 22150 |
</html>