The purpose of this investigation is to verify that the communication Static Context Header Compression and fragmentation (SCHC) framework ful lls the property of packet order and integrity. The standard will be modeled by state machines that represents the behaviour of the generic version and the LoRaWAN pro le of SCHC.
Internet de las cosas, IoT de Internet of Things, se reere a dispositivos f sicos conectados a internet. Estos dispositivos estan constantemente enviando una gran cantidad de datos a la red.
Para la conexion y env o de datos entre los dispositivos y hacia internet se utilizan redes LPWAN (LowPower Wide Area Networks), que son un tipo de comunicacion inalambrica disen~ada para conectar una gran cantidad de dispositivos IoT en una amplia area de cobertura utilizando poca energ a.
SCHC (Static Context Header Compression and Fragmentation) es un estandar que describe la compresion y fragmentacion de headers de los paquetes en redes LPWAN. Este estandar se puede adaptar a cualquier tecnolog a LPWAN.
La veri cacion de modelos o Model checking nos permite describir el comportamiento de un sistema y veri car propiedades sobre el mismo [Baier2008]. Para esto, se utilizan maquinas de estados, estas consisten en un conjunto de estados que mediante una funcion de transicion determinan el estado de un sistema en un determinado instante. 2
Para realizar model checking sobre SCHC el primer paso es construir el modelo que representa el comportamiento de la version general de SCHC. Las maquinas de estado son utilizadas para representar protocolos de comunicacion. El RF C8724 que describe SCHC [Min2020], indica las maquinas de estado para los tres modos de transmision: No-ACK, ACK-Always y ACK-on-Error, tanto para el dispositivo que env a datos como para el que los recibe.
Las propiedades que se quieren veri car en el modelo corresponden a veri car que los paquetes llegan en orden, que el sistema no queda en deadlock y en el caso de que ocurra, saber la probabilidad de se llegue a este estado.
Los modelos seran implementados en Promela, lenguaje que permite realizar model checking y as veri car si las propiedades de nidas anteriormente se cumplen.
Ademas, se construira la maquina de estado para representar el per l LoRaWAN de SCHC, para vericar que las propiedades que se cumplen en el modelo generico, tambien se cumplen en el per l LoRaWAN de SCHC. 3
Finalizado el modelamiento y veri cacion de las propiedades en el modelo generico y el per l de LoRaWAN, se espera encontrar que ambos modelos cumplen las mismas propiedades.
Como trabajo futuro queda optimizar los modelos, para esto, se pueden buscar optimizaciones sobre las maquinas de estados y as disminuir el tiempo de computo necesario para realizar model checking sobre los modelos. Este trabajo es nanciado por ANID FONDECYT 1201893.