Hacia la adaptación al crédito europeo en autómatas y lenguajes formales

Durante el curso 2006-2007 la asignatura Autómatas y Lenguajes Formales se ha incorporado al proyecto SICRE (Seguimiento para la Introducción de los CRéditos Europeos). El presente documento recoge cuál ha sido la orientación de la asignatura, principalmente en cuanto a actividades realizadas y resultados de las mismas.

Complemento práctico en la enseñanza de lenguajes formales usando las expresiones regulares en el contexto de aplicaciones web

Tradicionalmente la enseñanza de los autómatas y lenguajes formales basa su principal aplicación práctica en la construcción de compiladores. Sin embargo, las tareas de diseño y programación necesarias son excesivamente complejas como para que los estudiantes, que están cursando el tercer cuatrimestre de la Ingeniería, puedan abordarlas con el rigor necesario. Es posible incorporar otro enfoque práctico, real y más actual de las expresiones regulares en estas asignaturas, aprovechando su frecuente uso como herramienta de especificación de patrones a la hora de diseñar formularios de entrada de datos en diferentes contextos y, particularmente, en aplicaciones web de tres capas. El hecho de trabajar esta competencia junto con el desarrollo teórico de las expresiones regulares permite a los estudiantes ser conscientes de la importante utilidad práctica de este concepto, sin restringirlo a otros usos más clásicos relacionados con el diseño de procesadores de textos o analizadores léxicos. Durante el curso 2006-07 se ha propuesto a los estudiantes de Ingeniería Técnica en Informática de Sistemas de la Universidad del País Vasco desarrollar fragmentos de código basados en una notación formal para resolver problemas de reconocimiento de patrones. La experiencia se ha llevado a cabo utilizando concretamente la notación, inspirada en las expresiones regulares, de JavaScript, resultando viable, efectiva y bien valorada por parte de los estudiantes.

Solución para la delegación de identidad en Sistemas de Gestión de Identidad paneuropeos basada en infraestructuras de certificación y lenguajes formales de asertos de seguridad

La estrategia i2010 de la UE tiene como objetivo garantizar el liderazgo europeo en materia de TIC y poner los beneficios de la Sociedad de la Información al servicio de la economía, la sociedad y la calidad de vida personal, teniendo presente que los éxitos de Europa hasta la fecha se han basado en favorecer la competencia leal en los mercados de las telecomunicaciones y crear un mercado sin fronteras para contenidos y medios de comunicación digitales. En esta línea, la Comisión Europea ha establecido que los distintos estados miembros deben contribuir activamente al desarrollo y uso seguro de los servicios telemáticos entre sus ciudadanos. Más concretamente, atribuye a las Administraciones Públicas, tanto a nivel nacional, regional como local, un papel dinamizador de la Sociedad de la Información que les obliga a ofrecer paulatinamente todos los actos administrativos a los ciudadanos a través de Internet. Como primer paso para el uso seguro de los servicios telemáticos que ofrecen las instituciones públicas se hace preciso dotar a los ciudadanos de una identidad digital que les permita identificarse ante un Proveedor de Servicio o ante otros ciudadanos de manera inequívoca. Por esta razón, la mayoría de países europeos – y otros en el resto del mundo – están promoviendo, sistemas fiables de gestión de identidad electrónica (eIDM), de tal manera que los ciudadanos, las empresas y departamentos gubernamentales (incluso en Estados miembros diferentes) pueden identificar y certificar sus operaciones con precisión, rapidez y sencillez. Sin embargo, la gestión de esta identidad por las Administraciones Públicas supone un importante desafío, acentuado cuando se hace necesaria la interoperabilidad entre Administraciones de diferentes países, puesto que personas y entidades tienen credenciales de identificación diferentes en función de su propio marco jurídico nacional. Consciente del problema, en la Unión Europea se han puesto en marcha una serie de proyectos con el objetivo de conseguir la interoperabilidad de los eIDMs entre las instituciones públicas de diferentes Estados miembros. A pesar de ello, las soluciones adoptadas hasta la fecha son insuficientes porque no prevén todos los posibles casos de interacción del usuario con las instituciones. En concreto, no tienen en cuenta un aspecto muy importante que se ofrece en los distintos sistemas jurídicos nacionales, a saber, la delegación de la identidad, mediante la cual un ciudadano puede autorizar a otro para que actúe en su nombre para acceder a determinados servicios prestados por las instituciones públicas. En esta tesis se realizan un conjunto de aportaciones que dan solución a distintos aspectos de los problemas planteados y que, de forma conjunta, permiten la interoperabilidad y la delegación de identidad en determinados Sistemas de Gestión de Identidad aplicados al entorno de las Administraciones Públicas. En el caso de la delegación, se ha definido un sistema de delegación dinámica de identidad entre dos entidades genéricas que permite solucionar el problema del acceso delegado a los servicios telemáticos ofrecidos por las Administraciones Públicas. La solución propuesta se basa en la generación de un token de delegación, constituido a partir de un Certificado Proxy, que permite a la entidad que delega establecer la delegación de identidad en otra entidad en base a un subconjunto de sus atributos como delegador, estableciendo además, en el propio token de delegación, restricciones en el conjunto de servicios accesibles a la entidad delegada y el tiempo de validez de la delegación. Adicionalmente, se presentan los mecanismos necesarios tanto para poder revocar un token de delegación como para comprobar sin un token de delegación ha sido o no revocado. Para ello se propone una solución para la identificación unívoca de tokens de delegación y la creación de una nueva entidad denominada Autoridad de Revocación de Tokens de Delegación. Entre las características del sistema de delegación propuesto destaca el que es lo suficientemente seguro como para ser utilizado en el entorno de la Administración Pública, que no requiere el uso de mecanismos off‐line para la generación de la delegación y que se puede realizar la delegación de forma instantánea y sin la necesidad de trámites complejos o la participación de un elevado número de entidades. Adicionalmente, el token de delegación propuesto es perfectamente integrable en las infraestructura de clave pública actual lo que hace que, dado que gran parte de las Administraciones Públicas europeas basan sus sistemas de identidad digital en el uso de la PKI y certificados de identidad X.509, la solución pueda ser puesta en marcha en un entorno real sin necesidad de grandes cambios o modificaciones de comportamiento. En lo referente a la interoperabilidad, se realiza un análisis exhaustivo y la correspondiente evaluación de las principales propuestas de Sistemas de Gestión de Identidad orientados a conseguir la interoperabilidad realizadas hasta la fecha en el marco de la Unión Europea y se propone, a alto nivel, una arquitectura de interoperabilidad para la gestión de identidad en las Administraciones Públicas. Dicha arquitectura es lo suficientemente genérica como para poder ser aplicada tanto en el entorno pan‐Europeo como en los entornos nacionales, autonómicos y locales, de tal forma que la interoperabilidad en la gestión de la identidad esté garantizada en todos los niveles de la Administración Pública. Por último, mediante la integración de la solución de delegación dinámica de identidad y la arquitectura de interoperabilidad propuestas se presenta una solución al problema de la delegación en un escenario pan‐Europeo de gestión de identidad, dando lugar a una arquitectura global de interoperabilidad pan‐Europea con soporte a la delegación de identidad. SUMMARY The i2010 European Union Plan aims to ensure European leadership in ICT and to promote the positive contribution that information and communication technologies can make to the economic, social and personal quality of life, bearing in mind that, to date, success in Europe has been based on promoting fair competition in telecommunications markets and on creating a borderless market for contents and digital media. In this line, the European Commission has established that the different member states should contribute actively to the development and secure use of telematic services among their citizens. More specifically, it is attributed to national, regional and local Public Administrations to have a supportive role of the Information Society, requiring them to gradually provide the citizens with Internet‐based access to all administrative procedures acts. As a first step for the secure use of telematic services offered by public institutions, it is necessary to provide the citizens with a digital identity to enable them to identify themselves unequivocally to a Service Provider or to other citizens. For this reason, most European countries ‐ and others in the rest of the world ‐ are promoting reliable systems for managing electronic identity (eIDM), so that citizens, businesses and government departments (even in different Member States) can identify and certify their operations with precision, speed and simplicity. However, the identity management by Public Administrations is a major challenge that becomes more difficult when interoperability between administrations of different countries is needed, due to the fact that individuals and entities have different identification credentials according to their own national legal framework. Aware of the problem, the European Union has launched a series of projects with the aim of achieving interoperability of eIDMs between public institutions of different Member States. However, the solutions adopted to date are insufficient because they do not foresee all possible cases of user interaction with the institutions. In particular, solutions do not take into account a very important aspect that is offered in different national legal systems, namely, the delegation of identity, by which a citizen can authorize another to act on his/her behalf to access certain services provided by public institutions. In this thesis a collection of contributions that provide solution to different aspects of the aforementioned problems are carried out. The solutions, in global, enable interoperability and identity delegation in some of the Identity Management Systems applied to Public Administration environment. In the case of delegation, a dynamic identity delegation system between generic entities is defined. This system makes it possible to solve the problem of delegated access to telematic services offered by Public Administrations. The proposed solution is based on the generation of a piece of information called delegation token. This delegation token, derived from a Proxy Certificate, allows the establishment of identity delegation by an entity that delegates (delegator) in other entity (delegatee) making use of a subset of delegator attributes. It also establishes restrictions on services that can be used by the delegated entity and the expiry date of delegation. In addition to this, the mechanisms necessary to revoke and check the revocation status of a delegation token are presented. To do this, a solution to univocally identify delegation tokens and the creation of a completely new entity, called Token Delegation Revocation Authority, are proposed. The most remarkable characteristics of the proposed delegation system are its security, enough for it to be used in the Public Administration environment, the fact that it does not require off‐line processes in order to generate the delegation, and the possibility of performing the delegation instantaneously and without neither complex processes nor the intervention of a large number of entities. The proposed delegation token can be completely incorporated into current Public Key Infrastructure (PKI). Thus, since most of the European Public Administrations base their digital identity systems on PKI and X.509 identity certificates, the solution can be adopted in a real environment without great changes or performance modifications. Regarding interoperability, an exhaustive analysis and evaluation of most significant proposals on Identity Management Systems that aim to achieve interoperability carried out in the European Union framework until now are performed. A high level identity management interoperability architecture for Public Administrations is also proposed. This architecture is sufficiently generic to be applied to both pan‐European environment and national, regional or local environments, thus interoperability in identity management at all Public Administration levels is guaranteed. Finally, through the integration of the proposed dynamic identity delegation solution and the high level interoperability architecture, a solution to the problem of identity delegation in a pan‐European identity management environment is suggested, leading to a pan‐European global interoperability architecture with identity delegation support.

De la astronomía a la lingüística : una experiencia didáctica en torno a los logaritmos.

Resumen de los autores

Un mecanismo semántico aplicado a la documentación automática.

El Mecanismo Semántico aplicado a la documentación automática, es un esquema matemático que unifica diferentes aspectos del Reconocimiento de Formas, Lenguajes Formales y Diagnóstico Automático. Sin embargo se presenta sólo el Mecanismo proyectado en su aplicación al problema de la Clasificación e Interpretación Automática de Documentos. Se señalan las causas de esta delimitación. Por otro lado se tratan los siguientes puntos: en primer lugar se presenta un modelo para un posterior desarrollo, que introduce la noción de proyectividad de una manera natural en el concepto de diccionario, fundamental en la Lingüística matemática. En segundo lugar se analiza el teorema 2.10, de gran interés en cuestiones relacionadas con los algoritmos paralelos. En este mismo punto se define un modelo aplicable a diversos modelos analíticos lingüísticos. En tercer lugar se presenta un modelo que contiene, como caso particular, el algoritmo de Ferrari. Y por último se aplica el mecanismo a la clasificación de los documentos, previa interpretación de los conceptos.

Contribución a la automatización de sistemas de respuesta frente a intrusiones mediante ontologías

La seguridad en redes informáticas es un área que ha sido ampliamente estudiada y objeto de una extensa investigación en los últimos años. Debido al continuo incremento en la complejidad y sofisticación de los ataques informáticos, el aumento de su velocidad de difusión, y la lentitud de reacción frente a las intrusiones existente en la actualidad, se hace patente la necesidad de mecanismos de detección y respuesta a intrusiones, que detecten y además sean capaces de bloquear el ataque, y mitiguen su impacto en la medida de lo posible. Los Sistemas de Detección de Intrusiones o IDSs son tecnologías bastante maduras cuyo objetivo es detectar cualquier comportamiento malicioso que ocurra en las redes. Estos sistemas han evolucionado rápidamente en los últimos años convirtiéndose en herramientas muy maduras basadas en diferentes paradigmas, que mejoran su capacidad de detección y le otorgan un alto nivel de fiabilidad. Por otra parte, un Sistema de Respuesta a Intrusiones (IRS) es un componente de seguridad que puede estar presente en la arquitectura de una red informática, capaz de reaccionar frente a los incidentes detectados por un Sistema de Detección de Intrusiones (IDS). Por desgracia, esta tecnología no ha evolucionado al mismo ritmo que los IDSs, y la reacción contra los ataques detectados es lenta y básica, y los sistemas presentan problemas para ejecutar respuestas de forma automática. Esta tesis doctoral trata de hacer frente al problema existente en la reacción automática frente a intrusiones, mediante el uso de ontologías, lenguajes formales de especificación de comportamiento y razonadores semánticos como base de la arquitectura del sistema de un sistema de respuesta automática frente a intrusiones o AIRS. El objetivo de la aproximación es aprovechar las ventajas de las ontologías en entornos heterogéneos, además de su capacidad para especificar comportamiento sobre los objetos que representan los elementos del dominio modelado. Esta capacidad para especificar comportamiento será de gran utilidad para que el AIRS infiera la respuesta óptima frente a una intrusión en el menor tiempo posible. Abstract Security in networks is an area that has been widely studied and has been the focus of extensive research over the past few years. The number of security events is increasing, and they are each time more sophisticated, and quickly spread, and slow reaction against intrusions, there is a need for intrusion detection and response systems to dynamically adapt so as to better detect and respond to attacks in order to mitigate them or reduce their impact. Intrusion Detection Systems (IDSs) are mature technologies whose aim is detecting malicious behavior in the networks. These systems have quickly evolved and there are now very mature tools based on different paradigms (statistic anomaly-based, signature-based and hybrids) with a high level of reliability. On the other hand, Intrusion Response System (IRS) is a security technology able to react against the intrusions detected by IDS. Unfortunately, the state of the art in IRSs is not as mature as with IDSs. The reaction against intrusions is slow and simple, and these systems have difficulty detecting intrusions in real time and triggering automated responses. This dissertation is to address the existing problem in automated reactions against intrusions using ontologies, formal behaviour languages and semantic reasoners as the basis of the architecture of an automated intrusion response systems or AIRS. The aim is to take advantage of ontologies in heterogeneous environments, in addition to its ability to specify behavior of objects representing the elements of the modeling domain. This ability to specify behavior will be useful for the AIRS in the inference process of the optimum response against an intrusion, as quickly as possible.

Marco computacional para la definición de un modelo bio-inspirado en la señalización celular

Las Redes de Procesadores Evolutivos-NEP propuestas en [Mitrana et al., 2001], son un modelo computacional bio-inspirado a partir de la evolución de poblaciones de células, definiendo a nivel sintáctico algunas propiedades biológicas. En este modelo, las células están representadas por medio de palabras que describen secuencias de ADN. Informalmente, en algún instante de tiempo, el sistema evolutivo está representado por una colección de palabras cada una de las cuales representa una célula. El espacio genotipo de las especies, es un conjunto que recoge aquellas palabras que son aceptadas como sobrevivientes (es decir, como \correctas"). Desde el punto de vista de la evolución, las células pertenecen a especies y su comunidad evoluciona de acuerdo a procesos biológicos como la mutación y la división celular. éstos procesos representan el proceso natural de evolución y ponen de manifiesto una característica intrínseca de la naturaleza: el paralelismo. En este modelo, estos procesos son vistos como operaciones sobre palabras. Formalmente, el modelo de las NEP constituyen una arquitectura paralela y distribuida de procesamiento simbólico inspirada en la Máquina de conexión [Hillis, 1981], en el Paradigma de Flujo Lógico [Errico and Jesshope, 1994] y en las Redes de Procesadores Paralelos de Lenguajes (RPPL) [Csuhaj-Varju and Salomaa, 1997]. Al modelo NEP se han ido agregando nuevas y novedosas extensiones hasta el punto que actualmente podemos hablar de una familia de Redes de Procesadores Bio-inspirados (NBP) [Mitrana et al., 2012b]. Un considerable número de trabajos a lo largo de los últimos años han demostrado la potencia computacional de la familia NBP. En general, éstos modelos son computacionalmente completos, universales y eficientes [Manea et al., 2007], [Manea et al., 2010b], [Mitrana and Martín-Vide, 2005]. De acuerdo a lo anterior, se puede afirmar que el modelo NEP ha adquirido hasta el momento un nivel de madurez considerable. Sin embargo, aunque el modelo es de inspiración biológica, sus metas siguen estando motivadas en la Teoría de Lenguajes Formales y las Ciencias de la Computación. En este sentido, los aspectos biológicos han sido abordados desde una perspectiva cualitativa y el acercamiento a la realidad biológica es de forma meramente sintáctica. Para considerar estos aspectos y lograr dicho acercamiento es necesario que el modelo NEP tenga una perspectiva más amplia que incorpore la interacción de aspectos tanto cualitativos como cuantitativos. La contribución de esta Tesis puede considerarse como un paso hacia adelante en una nueva etapa de los NEPs, donde el carácter cuantitativo del modelo es de primordial interés y donde existen posibilidades de un cambio visible en el enfoque de interés del dominio de los problemas a considerar: de las ciencias de la computación hacia la simulación/modelado biológico y viceversa, entre otros. El marco computacional que proponemos en esta Tesis extiende el modelo de las Redes de Procesadores Evolutivos (NEP) y define arquitectura inspirada en la definición de bloques funcionales del proceso de señalización celular para la solución de problemas computacionales complejos y el modelado de fenómenos celulares desde una perspectiva discreta. En particular, se proponen dos extensiones: (1) los Transductores basados en Redes de Procesadores Evolutivos (NEPT), y (2) las Redes Parametrizadas de Procesadores Evolutivos Polarizados (PNPEP). La conservación de las propiedades y el poder computacional tanto de NEPT como de PNPEP se demuestra formalmente. Varias simulaciones de procesos relacionados con la señalización celular son abordadas sintáctica y computacionalmente, con el _n de mostrar la aplicabilidad e idoneidad de estas dos extensiones. ABSTRACT Network of Evolutionary Processors -NEP was proposed in [Mitrana et al., 2001], as a computational model inspired by the evolution of cell populations, which might model some properties of evolving cell communities at the syntactical level. In this model, cells are represented by words which encode their DNA sequences. Informally, at any moment of time, the evolutionary system is described by a collection of words, where each word represents one cell. Cells belong to species and their community evolves according to mutations and division which are defined by operations on words. Only those cells accepted as survivors (correct) are represented by a word in a given set of words, called the genotype space of the species. This feature is analogous with the natural process of evolution. Formally, NEP is based on an architecture for parallel and distributed processing inspired from the Connection Machine [Hillis, 1981], the Flow Logic Paradigm [Errico and Jesshope, 1994] and the Networks of Parallel Language Processors (RPPL) [Csuhaj-Varju and Salomaa, 1997]. Since the date when NEP was proposed, several extensions and variants have appeared engendering a new set of models named Networks of Bio-inspired Processors (NBP) [Mitrana et al., 2012b]. During this time, several works have proved the computational power of NBP. Specifically, their efficiency, universality, and computational completeness have been thoroughly investigated [Manea et al., 2007, Manea et al., 2010b, Mitrana and Martín-Vide, 2005]. Therefore, we can say that the NEP model has reached its maturity. Nevertheless, although the NEP model is biologically inspired, this model is mainly motivated by mathematical and computer science goals. In this context, the biological aspects are only considered from a qualitative and syntactical perspective. In view of this lack, it is important to try to keep the NEP theory as close as possible to the biological reality, extending their perspective incorporating the interplay of qualitative and quantitative aspects. The contribution of this Thesis, can be considered as a starting point in a new era of the NEP model. Then, the quantitative character of the NEP model is mandatory and it can address completely new different types of problems with respect to the classical computational domain (e.g. from the computer science to system biology). Therefore, the computational framework that we propose extends the NEP model and defines an architecture inspired by the functional blocks from cellular signaling in order to solve complex computational problems and cellular phenomena modeled from a discrete perspective. Particularly, we propose two extensions, namely: (1) Transducers based on Network of Evolutionary Processors (NEPT), and (2) Parametrized Network of Polarized Evolutionary Processors (PNPEP). Additionally, we have formally proved that the properties and computational power of NEP is kept in both extensions. Several simulations about processes related with cellular signaling both syntactical and computationally have been considered to show the model suitability.

Applications of Formal Languages to Management of Manned and Unmanned Aircraft

En el futuro, la gestión del tráfico aéreo (ATM, del inglés air traffic management) requerirá un cambio de paradigma, de la gestión principalmente táctica de hoy, a las denominadas operaciones basadas en trayectoria. Un incremento en el nivel de automatización liberará al personal de ATM —controladores, tripulación, etc.— de muchas de las tareas que realizan hoy. Las personas seguirán siendo el elemento central en la gestión del tráfico aéreo del futuro, pero lo serán mediante la gestión y toma de decisiones. Se espera que estas dos mejoras traigan un incremento en la eficiencia de la gestión del tráfico aéreo que permita hacer frente al incremento previsto en la demanda de transporte aéreo. Para aplicar el concepto de operaciones basadas en trayectoria, el usuario del espacio aéreo (la aerolínea, piloto, u operador) y el proveedor del servicio de navegación aérea deben negociar las trayectorias mediante un proceso de toma de decisiones colaborativo. En esta negociación, es necesaria una forma adecuada de compartir dichas trayectorias. Compartir la trayectoria completa requeriría un gran ancho de banda, y la trayectoria compartida podría invalidarse si cambiase la predicción meteorológica. En su lugar, podría compartirse una descripción de la trayectoria independiente de las condiciones meteorológicas, de manera que la trayectoria real se pudiese calcular a partir de dicha descripción. Esta descripción de la trayectoria debería ser fácil de procesar usando un programa de ordenador —ya que parte del proceso de toma de decisiones estará automatizado—, pero también fácil de entender para un operador humano —que será el que supervise el proceso y tome las decisiones oportunas—. Esta tesis presenta una serie de lenguajes formales que pueden usarse para este propósito. Estos lenguajes proporcionan los medios para describir trayectorias de aviones durante todas las fases de vuelo, desde la maniobra de push-back (remolcado hasta la calle de rodaje), hasta la llegada a la terminal del aeropuerto de destino. También permiten describir trayectorias tanto de aeronaves tripuladas como no tripuladas, incluyendo aviones de ala fija y cuadricópteros. Algunos de estos lenguajes están estrechamente relacionados entre sí, y organizados en una jerarquía. Uno de los lenguajes fundamentales de esta jerarquía, llamado aircraft intent description language (AIDL), ya había sido desarrollado con anterioridad a esta tesis. Este lenguaje fue derivado de las ecuaciones del movimiento de los aviones de ala fija, y puede utilizarse para describir sin ambigüedad trayectorias de este tipo de aeronaves. Una variante de este lenguaje, denominada quadrotor AIDL (QR-AIDL), ha sido desarrollada en esta tesis para permitir describir trayectorias de cuadricópteros con el mismo nivel de detalle. Seguidamente, otro lenguaje, denominado intent composite description language (ICDL), se apoya en los dos lenguajes anteriores, ofreciendo más flexibilidad para describir algunas partes de la trayectoria y dejar otras sin especificar. El ICDL se usa para proporcionar descripciones genéricas de maniobras comunes, que después se particularizan y combinan para formar descripciones complejas de un vuelo. Otro lenguaje puede construirse a partir del ICDL, denominado flight intent description language (FIDL). El FIDL especifica requisitos de alto nivel sobre las trayectorias —incluyendo restricciones y objetivos—, pero puede utilizar características del ICDL para proporcionar niveles de detalle arbitrarios en las distintas partes de un vuelo. Tanto el ICDL como el FIDL han sido desarrollados en colaboración con Boeing Research & Technology Europe (BR&TE). También se ha desarrollado un lenguaje para definir misiones en las que interactúan varias aeronaves, el mission intent description language (MIDL). Este lenguaje se basa en el FIDL y mantiene todo su poder expresivo, a la vez que proporciona nuevas semánticas para describir tareas, restricciones y objetivos relacionados con la misión. En ATM, los movimientos de un avión en la superficie de aeropuerto también tienen que ser monitorizados y gestionados. Otro lenguaje formal ha sido diseñado con este propósito, llamado surface movement description language (SMDL). Este lenguaje no pertenece a la jerarquía de lenguajes descrita en el párrafo anterior, y se basa en las clearances (autorizaciones del controlador) utilizadas durante las operaciones en superficie de aeropuerto. También proporciona medios para expresar incertidumbre y posibilidad de cambios en las distintas partes de la trayectoria. Finalmente, esta tesis explora las aplicaciones de estos lenguajes a la predicción de trayectorias y a la planificación de misiones. El concepto de trajectory language processing engine (TLPE) se usa en ambas aplicaciones. Un TLPE es una función de ATM cuya principal entrada y salida se expresan en cualquiera de los lenguajes incluidos en la jerarquía descrita en esta tesis. El proceso de predicción de trayectorias puede definirse como una combinación de TLPEs, cada uno de los cuales realiza una pequeña sub-tarea. Se le ha dado especial importancia a uno de estos TLPEs, que se encarga de generar el perfil horizontal, vertical y de configuración de la trayectoria. En particular, esta tesis presenta un método novedoso para la generación del perfil vertical. El proceso de planificar una misión también se puede ver como un TLPE donde la entrada se expresa en MIDL y la salida consiste en cierto número de trayectorias —una por cada aeronave disponible— descritas utilizando FIDL. Se ha formulado este problema utilizando programación entera mixta. Además, dado que encontrar caminos óptimos entre distintos puntos es un problema fundamental en la planificación de misiones, también se propone un algoritmo de búsqueda de caminos. Este algoritmo permite calcular rápidamente caminos cuasi-óptimos que esquivan todos los obstáculos en un entorno urbano. Los diferentes lenguajes formales definidos en esta tesis pueden utilizarse como una especificación estándar para la difusión de información entre distintos actores de la gestión del tráfico aéreo. En conjunto, estos lenguajes permiten describir trayectorias con el nivel de detalle necesario en cada aplicación, y se pueden utilizar para aumentar el nivel de automatización explotando esta información utilizando sistemas de soporte a la toma de decisiones. La aplicación de estos lenguajes a algunas funciones básicas de estos sistemas, como la predicción de trayectorias, han sido analizadas. ABSTRACT Future air traffic management (ATM) will require a paradigm shift from today’s mainly tactical ATM to trajectory-based operations (TBOs). An increase in the level of automation will also relieve humans —air traffic control officers (ATCOs), flight crew, etc.— from many of the tasks they perform today. Humans will still be central in this future ATM, as decision-makers and managers. These two improvements (TBOs and increased automation) are expected to provide the increase in ATM performance that will allow coping with the expected increase in air transport demand. Under TBOs, trajectories are negotiated between the airspace user (an airline, pilot, or operator) and the air navigation service provider (ANSP) using a collaborative decision making (CDM) process. A suitable method for sharing aircraft trajectories is necessary for this negotiation. Sharing a whole trajectory would require a high amount of bandwidth, and the shared trajectory might become invalid if the weather forecast changed. Instead, a description of the trajectory, decoupled from the weather conditions, could be shared, so that the actual trajectory could be computed from this trajectory description. This trajectory description should be easy to process using a computing program —as some of the CDM processes will be automated— but also easy to understand for a human operator —who will be supervising the process and making decisions. This thesis presents a series of formal languages that can be used for this purpose. These languages provide the means to describe aircraft trajectories during all phases of flight, from push back to arrival at the gate. They can also describe trajectories of both manned and unmanned aircraft, including fixedwing and some rotary-wing aircraft (quadrotors). Some of these languages are tightly interrelated and organized in a language hierarchy. One of the key languages in this hierarchy, the aircraft intent description language (AIDL), had already been developed prior to this thesis. This language was derived from the equations of motion of fixed-wing aircraft, and can provide an unambiguous description of fixed-wing aircraft trajectories. A variant of this language, the quadrotor AIDL (QR-AIDL), is developed in this thesis to allow describing a quadrotor aircraft trajectory with the same level of detail. Then, the intent composite description language (ICDL) is built on top of these two languages, providing more flexibility to describe some parts of the trajectory while leaving others unspecified. The ICDL is used to provide generic descriptions of common aircraft manoeuvres, which can be particularized and combined to form complex descriptions of flight. Another language is built on top of the ICDL, the flight intent description language (FIDL). The FIDL specifies high-level requirements on trajectories —including constraints and objectives—, but can use features of the ICDL to provide arbitrary levels of detail in different parts of the flight. The ICDL and FIDL have been developed in collaboration with Boeing Research & Technology Europe (BR&TE). Also, the mission intent description language (MIDL) has been developed to allow describing missions involving multiple aircraft. This language is based on the FIDL and keeps all its expressive power, while it also provides new semantics for describing mission tasks, mission objectives, and constraints involving several aircraft. In ATM, the movement of aircraft while on the airport surface also has to be monitored and managed. Another formal language has been designed for this purpose, denoted surface movement description language (SMDL). This language does not belong to the language hierarchy described above, and it is based on the clearances used in airport surface operations. Means to express uncertainty and mutability of different parts of the trajectory are also provided. Finally, the applications of these languages to trajectory prediction and mission planning are explored in this thesis. The concept of trajectory language processing engine (TLPE) is used in these two applications. A TLPE is an ATM function whose main input and output are expressed in any of the languages in the hierarchy described in this thesis. A modular trajectory predictor is defined as a combination of multiple TLPEs, each of them performing a small subtask. Special attention is given to the TLPE that builds the horizontal, vertical, and configuration profiles of the trajectory. In particular, a novel method for the generation of the vertical profile is presented. The process of planning a mission can also be seen as a TLPE, where the main input is expressed in the MIDL and the output consists of a number of trajectory descriptions —one for each aircraft available in the mission— expressed in the FIDL. A mixed integer linear programming (MILP) formulation for the problem of assigning mission tasks to the available aircraft is provided. In addition, since finding optimal paths between locations is a key problem to mission planning, a novel path finding algorithm is presented. This algorithm can compute near-shortest paths avoiding all obstacles in an urban environment in very short times. The several formal languages described in this thesis can serve as a standard specification to share trajectory information among different actors in ATM. In combination, these languages can describe trajectories with the necessary level of detail for any application, and can be used to increase automation by exploiting this information using decision support tools (DSTs). Their applications to some basic functions of DSTs, such as trajectory prediction, have been analized.

Enseñando a programar: un camino directo para desarrollar el pensamiento computacional

Está ampliamente aceptado que es fundamental desarrollar la habilidad de resolver problemas. El pensamiento computacional se basa en resolver problemas haciendo uso de conceptos fundamentales de la informática. Nada mejor para desarrollar la habilidad de resolver problemas usando conceptos informáticos que una asignatura de introducción a la programación. Este trabajo presenta nuestras reflexiones acerca de cómo iniciar a un estudiante en el campo de la programación de computadores. El trabajo no detalla los contenidos a impartir, sino que se centra en aspectos metodológicos, con la inclusión de experiencias y ejemplos concretos, a la vez que generales, extensibles a cualquier enseñanza de programación. En general, aunque se van desarrollado lenguajes cada vez más cercanos al lenguaje humano, la programación de ordenadores utilizando lenguajes formales no es una materia intuitiva y de fácil comprensión por parte de los estudiantes. A la persona que ya sabe programar le parece una tarea sencilla, pero al neófito no. Es más, dominar el arte de la programación es complejo. Por esta razón es indispensable utilizar todas las técnicas y herramientas posibles que faciliten dicha labor.

Tipologías del texto crítico en el arte y en la arquitectura. La creación de los lenguajes

386 p. : il. col.

Tipologías del texto crítico en el arte y en la arquitectura. La creación de los lenguajes

355 p.

Mecanización de semántica de lenguajes de programación: teoría, implementación y desarrollo.

El presente proyecto se enmarca en el área de métodos formales para computación; el objetivo de los métodos formales es asegurar, a través de herramientas lógicas y matemáticas, que sistemas computacionales satisfacen ciertas propiedades. El campo de semántica de lenguajes de programación trata justamente de construir modelos matemáticos que den cuenta de las diferentes características de cada lenguaje (estado mutable, mecanismos de paso de parámetros, órdenes de ejecución, etc.); permitiendo razonar de una manera abstracta, en vez de lidiar con las peculiaridades de implementaciones o las vaguezas de descripciones informales. Como las pruebas formales de corrección son demasiado intrincadas, es muy conveniente realizar estos desarrollos teóricos con la ayuda de asistentes de prueba. Este proceso de formalizar y corrobar aspectos semánticos a través de un asistente se denomina mecanización de semántica. Este proyecto – articulado en tres líneas: semántica de teoría de tipos, implementación de un lenguaje con tipos dependientes y semántica de lenguajes imperativos con alto orden - se propone realizar avances en el estudio semántico de lenguajes de programación, mecanizar dichos resultados, e implementar un lenguaje con tipos dependientes con la intención de que se convierta, en un mediano plazo, en un asistente de pruebas. En la línea de semántica de teoría de tipos los objetivos son: (a) extender el método de normalización por evaluación para construcciones no contempladas aun en la literatura, (b) probar la adecuación de la implementación en Haskell de dicho método de normalización, y (c) construir nuevos modelos categóricos de teoría de tipos. El objetivo de la segunda línea es el diseño e implementación de un lenguaje con tipos dependientes con la intención de que el mismo se convierta en un asistente de pruebas. Una novedad de esta implementación es que el algoritmo de chequeo de tipos es correcto y completo respecto al sistema formal, gracias a resultados ya obtenidos; además la implementación en Haskell del algoritmo de normalización (fundamental para el type-checking) también tendrá su prueba de corrección. El foco de la tercera línea está en el estudio de lenguajes de programación que combinan aspectos imperativos (estado mutable) con características de lenguajes funcionales (procedimientos y funciones). Por un lado se avanzará en la mecanización de pruebas de corrección de compiladores para lenguajes Algollike. El segundo aspecto de esta línea será la definición de semánticas operacional y denotacional del lenguaje de programación Lua y la posterior caracterización del mismo a partir de ellas. Para lograr dichos objetivos hemos dividido las tareas en actividades con metas graduales y que constituyen en sí mismas aportes al estado del arte de cada una de las líneas. La importancia académica de este proyecto radica en los avances teóricos que se propone en la línea de semántica de teoría de tipos, en las contribución para la construcción de pruebas mecanizadas de corrección de compiladores, en el aporte que constituye la definición de una semántica formal para el lenguaje Lua, y en el desarrollo de un lenguaje con tipos dependientes cuyos algoritmos más importantes están respaldados por pruebas de corrección. Además, a nivel local, este proyecto permitirá incorporar cuatro integrantes al grupo de “Semántica de la programación”.

Problemas formales de la traducción de The Shepheards Calender de Edmund Spenser

Eguíluz, Federico; Merino, Raquel; Olsen, Vickie; Pajares, Eterio; Santamaría, José Miguel (eds.)

El lenguaje en la política vasca: tres corrientes, tres lenguajes (1996-2004)

487 p. : il., col.