Specifying mobile network using a wp-like formal approach

  • Awadhesh Kumar Singh Department of Computer Engineering, National Institute of Technology, Kurukshetra 136119, India
  • Umesh Ghanekar Department of Electronics and Communication Engineering, National Institute of Technology, Kurukshetra 136119 India
  • Anup Kumar Bandyopadhyay Department of Electronics and Telecommunication Engineering, Jadavpur University, Kolkata 700032, India
Resumen Cómo citar Descargas

Resumen

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.
Cómo citar
Kumar Singh, A., Ghanekar, U., & Bandyopadhyay, A. K. (2005). Specifying mobile network using a wp-like formal approach. Revista Colombiana De Computación, 6(2), 1-19. Recuperado a partir de https://revistas.unab.edu.co/index.php/rcc/article/view/1063

Descargas

La descarga de datos todavía no está disponible.
Publicado
2005-12-01
Número
Vol. 6 Núm. 2 (2005): Revista Colombiana de Computación
Sección
Artículo de investigación científica y tecnológica

Derechos de autor 2005 Revista Colombiana de Computación

Creative Commons License
Esta obra está bajo licencia internacional Creative Commons Reconocimiento-NoComercial-CompartirIgual 4.0.

La publicación de un artículo en la Revista Colombiana de Computación, requiere la autorización por parte del autor, a través del formato de cesión de derechos, el cual autoriza al Editor de esta Revista, para la reproducción parcial o total, con fines académicos, no comerciales, ni lucrativos, de acuerdo a la filosofía Open Access en sitios Web y en Internet como en redes, bases de datos bibliográficas, índices, directorios o cualquier otro medio de reproducción electrónica, haciendo referencia siempre al autor(a) y a la revista en mención, de acuerdo a lo estipulado en la Licencia Creative Commons Atribución-NoComercial-CompartirIgual 4.0 Internacional.