@article{Kumar Singh_Ghanekar_Bandyopadhyay_2005, title={Specifying mobile network using a wp-like formal approach}, volume={6}, url={https://revistas.unab.edu.co/index.php/rcc/article/view/1063}, abstractNote={<span style="font-size: xx-small;"><p align="justify">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.</p></span><em><span style="font-size: x-small; font-family: Times New Roman,Times New Roman;"><span style="font-size: x-small; font-family: Times New Roman,Times New Roman;">Keywords: weakest precondition, mobile computing, specification, verification, safety, handover.</span></span></em>}, number={2}, journal={Revista Colombiana de Computación}, author={Kumar Singh, Awadhesh and Ghanekar, Umesh and Bandyopadhyay, Anup Kumar}, year={2005}, month={dic.}, pages={1–19} }