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


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


La descarga de datos todavía no está disponible.
Artículo de investigación científica y tecnológica