Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen angezeigt.

Link zu dieser Vergleichsansicht

Beide Seiten der vorigen Revision Vorhergehende Überarbeitung
Nächste Überarbeitung Beide Seiten der Revision
forschung:applying_formal_methods_for_qos_provisioning_in_mobile_architectures [2009/09/24 16:18]
barakat 		forschung:applying_formal_methods_for_qos_provisioning_in_mobile_architectures [2009/09/24 16:22]
barakat
Zeile 470: Zeile 470:
 </​html>​ </​html>​
  
-</​html>​ 
  
 Π-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 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: ​
Zeile 491: Zeile 490:
 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: ​ 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: ​
  
-{{ :​forschung:​image011.jpg|Copyright OPNET Technologies,​ Inc.(r)}}+{{ :​forschung:​image011.jpg |Copyright OPNET Technologies,​ Inc.(r)}}
  
   * 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 LTE are going to be the RATs of our mobile routers.   * 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 LTE are going to be the RATs of our mobile routers.
Zeile 501: Zeile 500:
   * Collect baseline measurements against which QoS improvements are going to be evaluated.   * 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.   * 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.
 +
 +=== References ===
 +
 +  - 3GPP-23.401 General Packet Radio Service (GPRS) enhancements for Evolved Universal Terrestrial Radio Access Network (E-UTRAN) access.
 +  - 3GPP-23.402 Architecture enhancements for non-3GPP accesses.
 +  - 3GPP-22.259 Service requirements for Personal Network Management (PNM).
 +  - M. Abadi and A.D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Fourth ACM Conference on Computer and Communications Security, pages 36-47. ACM, 1997.
 +  - L. Cardelli and A. D. Gordon. Mobile ambients. In Foundations of Software Science and Computation Structures, Lisbon, 1998.
 +  - IETF-RFC3963 Network Mobility (NEMO) Basic Support Protocol.
 +  - IETF-RFC4980 Analysis of Multihoming in Network Mobility Support.
 +  - IETF-RFC3775 Mobility Support in IPv6.
 +  - R. Milner. Communicating and Mobile Systems: The pi-Calculus. Cambridge University Press, 1999.
 +  - R. Milner. The Polyadic π-calculus:​ a tutorial. ECS-LFCS-89-85 91-180, University of Edinburgh, 1991.
 +  - Claus Pahl, A PiCalculus based Framework for the Composition and Replacement of Components. In Workshop on Specification and Verification of Component-Based Systems (OOPSLA 2001), 2001.
 +
 +