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...

Full description

Bibliographic Details
Main Authors: Awadhesh Kumar Singh, Umesh Ghanekar, Anup Kumar Bandyopadhyay
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