Especificación de la red móvil mediante un enfoque formal similar a wp

Abstract

El documento tiene como objetivo proporcionar un sistema formal, motivado por la condición previa más débil de Dijkstra lógica, para especificar la red móvil. El documento muestra cómo se puede especificar la movilidad utilizando un enfoque basado en el estado y la transición, que permite que los hosts móviles sean tratados como nodos en un sistema distribuido estructurado estáticamente tradicional. Otro objetivo es razonar formalmente sobre la posibles comportamientos de un sistema formado por componentes móviles. El procedimiento de entrega sirve como una ilustración para la notación. La contribución del artículo es el desarrollo de un estilo de modelado y razonamiento sobre las propiedades temporales que permite una análisis exhaustivo de los sistemas móviles.