Verificación de extensiones de Redes de Petri con precios, tiempo y múltiples instancias

Las redes de Petri son un lenguaje formal muy adecuado para la modelizacíon, ańalisis y verificacíon de sistemas concurrentes con infinitos estados. En particular, son muy apropiadas para estudiar las propiedades de seguridad de dichos sistemas, dadas sus buenas propiedades de decidibilidad. Sin embargo, en muchas ocasiones las redes de Petri carecen de la expresividad necesaria para representar algunas caracteŕısticas fundamentales de los sistemas que se manejan hoy en d́ıa, como el manejo de tiempo real, costes reales, o la presencia de varios procesos con un ńumero no acotado de estados ejecut́andose en paralelo. En la literatura se han definido y estudiado algunas extensiones de las redes de Petri para la representaci ́on de las caracteŕısticas anteriores. Por ejemplo, las “Redes de Petri Temporizadas” [83, 10](TPN) incluyen el manejo de tiempo real y las ν-redes de Petri [78](ν-PN) son capaces de representar un ńumero no acotado de procesos con infinitos estados ejecut́andose concurrentemente. En esta tesis definimos varias extensiones que réunen estas dos caracteŕısticas y estudiamos sus propiedades de decidibilidad. En primer lugar definimos las “ν-Redes de Petri Temporizadas”, que réunen las caracteŕısticas expresivas de las TPN y las ν-PN. Este nuevo modelo es capaz de representar sistemas con un ńumero no acotado de procesos o instancias, donde cada proceso es representado por un nombre diferente, y tiene un ńumero no acotado de relojes reales. En este modelo un reloj de una instancia debe satisfacer ciertas condiciones (pertenecer a un intervalo dado) para formar parte en el disparo de una transicíon. Desafortunadamente, demostramos que la verificacíon de propiedades de seguridad es indecidible para este modelo...

Diseño y validación de políticas de transmisión de datos en redes inalámbricas de sensores de bajo consumo

El envejecimiento de la poblaci on, el sobrepeso, y el aumento de enfermedades cr onicas, tales como: afecciones cardiacas, diabetes e hipertensi on, plantean nuevos retos al sistema de salud p ublica. En este contexto, las redes de sensores inal ambricas corporales (Wireless Body Area Networks (WBAN)/Wireless Body Sensor Networks (WBSN)) tienen gran potencial para revolucionar el sistema de salud ya que facilitan el seguimiento, la monitorizaci on y el diagn ostico de pacientes en casa, mejorando as su calidad de vida y reduciendo los costes asociados la asistencia sanitaria. Las redes WBAN/WBSN est an constituidas por nodos sensores que miden diferentes variables siol ogicas y cin eticas y disponen de interfaces inal ambricas de bajo coste para transmitir en tiempo real la informaci on a dispositivos en otros niveles de la red. En este tipo de redes, la transmisi on inal ambrica de datos es probablemente la tarea que presenta mayor consumo de energ a, por lo que dicho consumo debe ser reducido para maximizar su vida util. Adicionalmente, en escenarios WBAN/WBSN, el cuerpo humano juega un papel muy importante en la calidad de la comunicaci on. El cuerpo act ua como un canal de comunicaci on para la propagaci on de ondas electromagn eticas, por lo que el comportamiento de este tipo de canal representa un conjunto unico de desaf os para la transferencia able de datos...

Nuevos ataques estadísticos de revelación de identidades en redes de comunicaciones anónimas

El anonimato es una dimensi on de la privacidad en la que una persona se reserva su identidad en las relaciones sociales que mantiene. Desde el punto de vista del area de las comunicaciones electr onicas, el anonimato posibilita mantener oculta la informaci on que pueda conducir a la identi caci on de las partes involucradas en una transacci on. Actualmente, conservar el anonimato en las transacciones de informaci on en red representa uno de los aspectos m as importantes. Con este n se han desarrollado diversas tecnolog as, com unmente denominadas tecnolog as para la mejora de la privacidad. Una de las formas m as populares y sencillas de proteger el anonimato en las comunicaciones entre usuarios son los sistemas de comunicaci on an onima de baja latencia basados en redes de mezcladores. Estos sistemas est an expuestos a una serie de ataques basados en an alisis de tr a co que comprometen la privacidad de las relaciones entre los usuarios participantes en la comunicaci on, esto es, que determinan, en mayor o menor medida, las identidades de emisores y receptores. Entre los diferentes tipos de ataques destacan los basados en la inundaci on de la red con informaci on falsa para obtener patrones en la red de mezcladores, los basados en el control del tiempo, los basados en el contenido de los mensajes, y los conocidos como ataques de intersecci on, que pretenden inferir, a trav es de razonamientos probabil sticos o de optimizaci on, patrones de relaciones entre usuarios a partir de la informaci on recabada en lotes o durante un per odo de tiempo por parte del atacante. Este ultimo tipo de ataque es el objeto de la presente tesis...

Diseño e implementación de una herramienta de visualización para análisis en tiempo real de redes SDN/OpenFlow

Las Redes Definidas por Software (Software Defined Networking) permiten la monitorización y el control centralizado de la red, de forma que los administradores pueden tener una visión real y completa de la misma. El análisis y visualización de los diferentes parámetros obtenidos representan la forma más viable y práctica de programar la red en función de las necesidades del usuario. Por este motivo, en este proyecto se desarrolla una arquitectura modular cuyo objetivo es presentar en tiempo real la información que se monitoriza en una red SDN. En primera instancia, las diferentes métricas monitorizadas (error, retardo y tasa de datos) son almacenadas en una base de datos, para que en una etapa posterior se realice el análisis de dichas métricas. Finalmente, los resultados obtenidos, tanto de métricas en tiempo real como de los datos estadísticos, son presentados en una aplicación web. La información es obtenida a través de la interfaz REST que expone el controlador Floodlight y para el análisis de la información se plantea una comparación entre los valores medios y máximos del conjunto de datos. Los resultados obtenidos muestran gráficamente de forma clara y precisa las diferentes métricas de monitorización. Además, debido al carácter modular de la arquitectura, se ofrece un valor añadido a los sistemas actuales de monitorización SDN.

System to predict bipolar disorder crises analysing massive data

Durante el desarrollo del proyecto he aprendido sobre Big Data, Android y MongoDB mientras que ayudaba a desarrollar un sistema para la predicción de las crisis del trastorno bipolar mediante el análisis masivo de información de diversas fuentes. En concreto hice una parte teórica sobre bases de datos NoSQL, Streaming Spark y Redes Neuronales y después diseñé y configuré una base de datos MongoDB para el proyecto del trastorno bipolar. También aprendí sobre Android y diseñé y desarrollé una aplicación de móvil en Android para recoger datos para usarlos como entrada en el sistema de predicción de crisis. Una vez terminado el desarrollo de la aplicación también llevé a cabo una evaluación con usuarios.