Hier werden die Unterschiede zwischen zwei Versionen angezeigt.
| Beide Seiten der vorigen Revision Vorhergehende Überarbeitung Nächste Überarbeitung | Vorhergehende Überarbeitung Nächste Überarbeitung Beide Seiten der Revision | ||
|
forschung:applying_formal_methods_for_qos_provisioning_in_mobile_architectures [2009/09/24 16:37] barakat |
forschung:applying_formal_methods_for_qos_provisioning_in_mobile_architectures [2009/09/24 16:42] barakat |
||
|---|---|---|---|
| Zeile 7: | Zeile 7: | ||
| === Work Plan === | === 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 between each other. 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. | 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 between each other. 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 === | === The Formal Model === | ||
| Zeile 479: | Zeile 480: | ||
| * 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. | * 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: | 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 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. | ||
| Zeile 486: | Zeile 488: | ||
| \\ | \\ | ||
| === Simulating the Protocol === | === Simulating the Protocol === | ||
| + | \\ | ||
| {{ :forschung:image009.jpg |Copyright OPNET Technologies, Inc.(r)}} | {{ :forschung:image009.jpg |Copyright OPNET Technologies, Inc.(r)}} | ||
| \\ | \\ | ||