Specifying mobile network using a wp-like formal approach
The paper aims at providing a formal system, motivated by Dijkstra’s weakest precondition logic, for specifying mobile network. The paper shows how mobility can be specified using a state and transition based approach, which allows mobile hosts to be treated as nodes in a traditional statically stru...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Universidad Autónoma de Bucaramanga
2005-12-01
|
Series: | Revista Colombiana de Computación |
Online Access: | https://revistas.unab.edu.co/index.php/rcc/article/view/1063 |
id |
doaj-07852f5e8d2846798327b4e4b811f8d3 |
---|---|
record_format |
Article |
spelling |
doaj-07852f5e8d2846798327b4e4b811f8d32020-11-25T03:32:24ZengUniversidad Autónoma de BucaramangaRevista Colombiana de Computación1657-28312539-21152005-12-0162Specifying mobile network using a wp-like formal approachAwadhesh Kumar Singh0Umesh Ghanekar1Anup Kumar Bandyopadhyay2Department of Computer Engineering, National Institute of Technology, Kurukshetra 136119, IndiaDepartment of Electronics and Communication Engineering, National Institute of Technology, Kurukshetra 136119 IndiaDepartment of Electronics and Telecommunication Engineering, Jadavpur University, Kolkata 700032, IndiaThe paper aims at providing a formal system, motivated by Dijkstra’s weakest precondition logic, for specifying mobile network. The paper shows how mobility can be specified using a state and transition based approach, which allows mobile hosts to be treated as nodes in a traditional statically structured distributed system. Another goal is to reason formally about the possible behaviors of a system consisting of mobile components. The handover procedure serves as an illustration for the notation. The contribution of the paper is the development of a style of modeling and reasoning about the temporal properties that allows for a straightforward and thorough analysis of mobile systems. Keywords: weakest precondition, mobile computing, specification, verification, safety, handover.https://revistas.unab.edu.co/index.php/rcc/article/view/1063 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Awadhesh Kumar Singh Umesh Ghanekar Anup Kumar Bandyopadhyay |
spellingShingle |
Awadhesh Kumar Singh Umesh Ghanekar Anup Kumar Bandyopadhyay Specifying mobile network using a wp-like formal approach Revista Colombiana de Computación |
author_facet |
Awadhesh Kumar Singh Umesh Ghanekar Anup Kumar Bandyopadhyay |
author_sort |
Awadhesh Kumar Singh |
title |
Specifying mobile network using a wp-like formal approach |
title_short |
Specifying mobile network using a wp-like formal approach |
title_full |
Specifying mobile network using a wp-like formal approach |
title_fullStr |
Specifying mobile network using a wp-like formal approach |
title_full_unstemmed |
Specifying mobile network using a wp-like formal approach |
title_sort |
specifying mobile network using a wp-like formal approach |
publisher |
Universidad Autónoma de Bucaramanga |
series |
Revista Colombiana de Computación |
issn |
1657-2831 2539-2115 |
publishDate |
2005-12-01 |
description |
The paper aims at providing a formal system, motivated by Dijkstra’s weakest precondition logic, for specifying mobile network. The paper shows how mobility can be specified using a state and transition based approach, which allows mobile hosts to be treated as nodes in a traditional statically structured distributed system. Another goal is to reason formally about the possible behaviors of a system consisting of mobile components. The handover procedure serves as an illustration for the notation. The contribution of the paper is the development of a style of modeling and reasoning about the temporal properties that allows for a straightforward and thorough analysis of mobile systems.
Keywords: weakest precondition, mobile computing, specification, verification, safety, handover. |
url |
https://revistas.unab.edu.co/index.php/rcc/article/view/1063 |
work_keys_str_mv |
AT awadheshkumarsingh specifyingmobilenetworkusingawplikeformalapproach AT umeshghanekar specifyingmobilenetworkusingawplikeformalapproach AT anupkumarbandyopadhyay specifyingmobilenetworkusingawplikeformalapproach |
_version_ |
1724568623631040512 |