Infrastructure and Workflow for the Formal Evaluation of Semantic Search Technologies

This paper describes an infrastructure for the automated evaluation of semantic technologies and, in particular, semantic search technologies. For this purpose, we present an evaluation framework which follows a service-oriented approach for evaluating semantic technologies and uses the Business Process Execution Language (BPEL) to define evaluation workflows that can be executed by process engines. This framework supports a variety of evaluations, from different semantic areas, including search, and is extendible to new evaluations. We show how BPEL addresses this diversity as well as how it is used to solve specific challenges such as heterogeneity, error handling and reuse

Formal verification of safety protocol in train control system

In order to satisfy the safety-critical requirements, the train control system (TCS) often employs a layered safety communication protocol to provide reliable services. However, both description and verification of the safety protocols may be formidable due to the system complexity. In this paper, interface automata (IA) are used to describe the safety service interface behaviors of safety communication protocol. A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN. A case study of using this method to describe and verify a safety communication protocol is included. The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks, livelocks and several mandatory consistency properties. A prototype of safety protocols is also developed based on the presented formally verifying method.

Relational and Allegorical Semantics for Constraint Logic Programming

El cálculo de relaciones binarias fue creado por De Morgan en 1860 para ser posteriormente desarrollado en gran medida por Peirce y Schröder. Tarski, Givant, Freyd y Scedrov demostraron que las álgebras relacionales son capaces de formalizar la lógica de primer orden, la lógica de orden superior así como la teoría de conjuntos. A partir de los resultados matemáticos de Tarski y Freyd, esta tesis desarrolla semánticas denotacionales y operacionales para la programación lógica con restricciones usando el álgebra relacional como base. La idea principal es la utilización del concepto de semántica ejecutable, semánticas cuya característica principal es el que la ejecución es posible utilizando el razonamiento estándar del universo semántico, este caso, razonamiento ecuacional. En el caso de este trabajo, se muestra que las álgebras relacionales distributivas con un operador de punto fijo capturan toda la teoría y metateoría estándar de la programación lógica con restricciones incluyendo los árboles utilizados en la búsqueda de demostraciones. La mayor parte de técnicas de optimización de programas, evaluación parcial e interpretación abstracta pueden ser llevadas a cabo utilizando las semánticas aquí presentadas. La demostración de la corrección de la implementación resulta extremadamente sencilla. En la primera parte de la tesis, un programa lógico con restricciones es traducido a un conjunto de términos relacionales. La interpretación estándar en la teoría de conjuntos de dichas relaciones coincide con la semántica estándar para CLP. Las consultas contra el programa traducido son llevadas a cabo mediante la reescritura de relaciones. Para concluir la primera parte, se demuestra la corrección y equivalencia operacional de esta nueva semántica, así como se define un algoritmo de unificación mediante la reescritura de relaciones. La segunda parte de la tesis desarrolla una semántica para la programación lógica con restricciones usando la teoría de alegorías—versión categórica del álgebra de relaciones—de Freyd. Para ello, se definen dos nuevos conceptos de Categoría Regular de Lawvere y _-Alegoría, en las cuales es posible interpretar un programa lógico. La ventaja fundamental que el enfoque categórico aporta es la definición de una máquina categórica que mejora e sistema de reescritura presentado en la primera parte. Gracias al uso de relaciones tabulares, la máquina modela la ejecución eficiente sin salir de un marco estrictamente formal. Utilizando la reescritura de diagramas, se define un algoritmo para el cálculo de pullbacks en Categorías Regulares de Lawvere. Los dominios de las tabulaciones aportan información sobre la utilización de memoria y variable libres, mientras que el estado compartido queda capturado por los diagramas. La especificación de la máquina induce la derivación formal de un juego de instrucciones eficiente. El marco categórico aporta otras importantes ventajas, como la posibilidad de incorporar tipos de datos algebraicos, funciones y otras extensiones a Prolog, a la vez que se conserva el carácter 100% declarativo de nuestra semántica. ABSTRACT The calculus of binary relations was introduced by De Morgan in 1860, to be greatly developed by Peirce and Schröder, as well as many others in the twentieth century. Using different formulations of relational structures, Tarski, Givant, Freyd, and Scedrov have shown how relation algebras can provide a variable-free way of formalizing first order logic, higher order logic and set theory, among other formal systems. Building on those mathematical results, we develop denotational and operational semantics for Constraint Logic Programming using relation algebra. The idea of executable semantics plays a fundamental role in this work, both as a philosophical and technical foundation. We call a semantics executable when program execution can be carried out using the regular theory and tools that define the semantic universe. Throughout this work, the use of pure algebraic reasoning is the basis of denotational and operational results, eliminating all the classical non-equational meta-theory associated to traditional semantics for Logic Programming. All algebraic reasoning, including execution, is performed in an algebraic way, to the point we could state that the denotational semantics of a CLP program is directly executable. Techniques like optimization, partial evaluation and abstract interpretation find a natural place in our algebraic models. Other properties, like correctness of the implementation or program transformation are easy to check, as they are carried out using instances of the general equational theory. In the first part of the work, we translate Constraint Logic Programs to binary relations in a modified version of the distributive relation algebras used by Tarski. Execution is carried out by a rewriting system. We prove adequacy and operational equivalence of the semantics. In the second part of the work, the relation algebraic approach is improved by using allegory theory, a categorical version of the algebra of relations developed by Freyd and Scedrov. The use of allegories lifts the semantics to typed relations, which capture the number of logical variables used by a predicate or program state in a declarative way. A logic program is interpreted in a _-allegory, which is in turn generated from a new notion of Regular Lawvere Category. As in the untyped case, program translation coincides with program interpretation. Thus, we develop a categorical machine directly from the semantics. The machine is based on relation composition, with a pullback calculation algorithm at its core. The algorithm is defined with the help of a notion of diagram rewriting. In this operational interpretation, types represent information about memory allocation and the execution mechanism is more efficient, thanks to the faithful representation of shared state by categorical projections. We finish the work by illustrating how the categorical semantics allows the incorporation into Prolog of constructs typical of Functional Programming, like abstract data types, and strict and lazy functions.

MotoStudent, un paradigma de emprendimiento y educación no formal en la universidad

Muchas instituciones de educación superior de todo el mundo llevan tiempo dinamizando sus enseñanzas a fin de transmitir a sus egresados las nuevas competencias que demanda la sociedad del siglo XXI. Afortunadamente en España también existe una fuerte apuesta por la flexibilización de la educación superior, que se materializa en iniciativas tales como la competición internacional MotoStudent.

La Esgrima como enseñanza formal en las instituciones educativas públicas de Madrid. Del Real Seminario de Nobles al Instituto de Segunda Enseñanza Cardenal Cisneros (1725-1950).

En el presente trabajo de investigación se ha analizado la presencia de la Esgrima como materia de enseñanza dentro de diversas Instituciones educativas formales de Madrid, abarcando un rango temporal de 225 años (1725-1950). Para la realización de la investigación se elaboró un esquema de trabajo basado en la metodología de la investigación histórica, la historiografía. La búsqueda de la información se llevó a cabo, fundamentalmente en el Archivo Histórico Nacional el Archivo General de la Administración, el Archivo Regional de Madrid, el Archivo General de la Universidad Complutense de Madrid, el Archivo del Real Conservatorio Superior de Música de Madrid, el Archivo General de Palacio, el Archivo de la Villa y la Biblioteca Nacional. La investigación presentada abarca cinco Instituciones educativas en las que se estudia la presencia de la Esgrima como enseñanza formal, siendo estas el Real Seminario de Nobles de Madrid, la Escuela Central de Profesores y Profesoras de Gimnástica, el Real Conservatorio de Música y Declamación y los Institutos de Segunda Enseñanza del Cardenal Cisneros y de San Isidro. Se analizaron las diferentes Constituciones de formación, Planes de Estudios, Reglamentos Interinos de funcionamiento, Leyes de fundación, libros, Programas de asignaturas y todos aquellos documentos, tanto oficiales como internos de cada uno de los Centros tratados. Así mismo, se estudiaron las figuras de los Maestros encargados de impartir la Esgrima como materia formal en las diversas Instituciones, alcanzando la mayor relevancia D. Manuel Antonio de Brea, D. Francisco de la Macorra y Guijeño, D. Ángel Lancho Martín de la Fuente, D. Afrodisio Aparicio Aparicio y D. José Carbonell. De la investigación realizada se concluye la presencia de la Esgrima como una materia perfectamente sistematizada en cada uno de las Instituciones analizadas así como la importancia que alcanzaba la figura del Maestro de Esgrima en todas ellas, siendo en algunos casos “Maestro Mayor del Reyno” y en otros convirtiéndose en Catedráticos de Esgrima, al tiempo que todos ellos contaban con una titulación que les capacitaba para el ejercicio de su profesión. Así mismo encontramos la presencia de la mujer en una de las Instituciones, el Real Conservatorio de Música y Declamación, con los mismos derechos que sus compañeros varones para matricularse y estudiar la Esgrima. Los Maestros estudiados, fundamentalmente D. Ángel Lancho, D. Afrodisio Aparicio y D. José Carbonell, contribuyeron a popularizar la Esgrima y a su desarrollo como deporte, organizando torneos para sus alumnos y compitiendo ellos mismos en multitud de asaltos. A lo largo de los 225 años que abarca esta investigación, la Esgrima evolucionó de Destreza a Habilidad y más tarde a Deporte, sin perder en ningún momento su importancia, extendiéndose a sectores de la sociedad a los que nunca habría llegado de no ser por la labor de los Maestros de Esgrima encargados de su formación. ABSTRACT. In this research work, the presence of Fencing as an educational subject within different formal educational Institutions in Madrid, over a period of 225 years (1725-1950), has been analysed. In order to carry out this research, a work schedule was drawn up, based on the methods of the historical research, historiography. The search for the information was primarily carried out in the Archivo Historico Nacional, the Archivo General de la Administración, the Archivo Regional of Madrid, the Archivo General de la Universidad Complutense de Madrid, the Archivo del Real Conservatorio Superior de Música of Madrid, the Archivo General de Palacio, the Archivo de la Villa and the Biblioteca Nacional. The research presented covers five educational Institutions, where the presence of Fencing as a formal education is studied. These Institutions are: the Real Seminario de Nobles de Madrid, the Escuela Central de Profesores y Profesoras de Gimnástica, the Real Conservatorio de Música y Declamación and the Cardenal Cisneros and the San Isidro Secondary Schools. The different Academic formation, Syllabuses, Temporary working Regulations, founding Law, books, subject Plans and all the documents, official or internal, of each of the Centres dealt with, were analysed. Moreover, the roles of the Masters in charge of teaching Fencing as a formal subject in different Institutions were studied, and Mr. Manuel Antonio de Brea, Mr. Francisco de la Macorra y Guijeño, Mr. Ángel Lancho Martín de la Fuente, Mr. Afrodisio Aparicio Aparicio and Mr. José Carbonell were the most prominent. The conclusion of the research carried out, is that the presence of Fencing is a subject perfectly organised in each one of the Institutions analysed, as well as the importance that the role of the Fencing Master reached in every Institution, in some cases being “Maestro Mayor del Reyno” and in others becoming Fencing Professors, while all of them had a qualification that enabled them to practice their profession. Similarly, we can find the presence of women in one of the Institutions, the Real Conservatorio de Música y Declamación, where they had the same rights as her male classmates to enrol and study Fencing. The Fencing Masters who were studied, principally Mr. Ángel Lancho, Mr. Afrodisio Aparicio and Mr. José Carbonell, all contributed to making Fencing popular and also towards its development as a sport, by organising tournaments for their students and by competing themselves in a number of assaults. Over the 225 years which the research covers, Fencing evolved from Skill to Ability and later on to a Sport, without, at any moment, losing its importance, spreading to parts of society that it would never have reached if it were not for the work of the Fencing Masters in charge of teaching it.

El dibujo como medio de investigación: recursos gráficos del análisis formal

Ponencia sobre el dibujo de arquitectura como medio de investigación.

Aplicación de algoritmos paramétricos de generación formal en el diseño estructural. La Ópera de Sídney desde una perspectiva contemporánea.

El importante desarrollo tecnológico e industrial surgido especialmente durante la segunda mitad del siglo pasado ha eliminado las históricas limitaciones técnicas en el ámbito de los pro-­? yectos arquitectónicos, desembocando en la situación actual en la que cualquier planteamiento formal puede ser analizado desde un punto de vista estructural, concluyéndose por tanto que ha desaparecido la barrera del análisis en lo que al desarrollo de un proyecto arquitectónico se refiere. En la actualidad, al igual que a finales del siglo XIX, nos encontramos en un periodo de transi-­? ción, y también, como entonces, es la tecnología la que orienta el cambio. No la tecnología de los nuevos materiales (hormigón y acero) como sucedía tras la revolución industrial sino que es la nueva tecnología digital aplicada a los sistemas de diseño, cálculo y fabricación la que están siendo el motor de la actual transformación. Hoy no es tanto el paradigma mecanicista el que prevalece en muchos casos en la concepción de los edificios sino que, nuevos elementos como la tecnología digital integrada está cambiando la forma de diseñar y concebir el entorno cons-­? truido. Ante este contexto cabría plantearse las siguientes cuestiones: ¿Puede el diseño paramétrico y la tecnología CAD-­?CAM-­?CAE en conjunción con los programas actuales de análisis estructural basados en el Método de los Elementos Finitos hacer más sencilla la construcción de estructu-­? ras ligeras y eficientes hoy en día? ¿Puede la tecnología digital ayudar a ampliar el abanico for-­? mal a la hora de diseñar edificios y a la vez permitir el uso de sistemas estructurales racionales que optimicen el consumo de materiales bajo dichas circunstancias?

MotoStudent, un paradigma de emprendimiento y educación no formal en la universidad

Resumen: Muchas instituciones de educación superior de todo el mundo llevan tiempo dinamizando sus enseñanzas a fin de transmitir a sus egresados las nuevas competencias que demanda la sociedad del siglo XXI. Afortunadamente en España también existe una fuerte apuesta por la flexibilización de la educación superior, que se materializa en iniciativas tales como la competición internacional MotoStudent. Abstract: A lot of educational superior institutions around the world have been dynamized their teaching methods trying to transmit to their graduates the new abilities that demands the XX’s century society. Fortunately in Spain it also exist a hard bet for the flexibility of the high education, materialized in initiatives as the international “MotoStudent” contest.

Fragmentación formal y simplificación funcional de la ciudad de Tacubaya, dentro de la metrópoli de México, durante los procesos de expansión de la primera mitad del siglo XX

La fragmentación espacial de una ciudad, que será el principal enfoque de la presente Tesis, ocurre cuando una entidad pequeña se ve obligada a adecuar sus relaciones ante la inminente presencia de un entorno urbano de mayor peso que se aproxima y densifica. Este tipo de fragmentación se analizará tomando en cuenta tres factores (especulación, desorganización y falta de protección) que moldean el desarrollo de procesos urbanísticos modernos en las grandes metrópolis Latinoamericanas, particularmente en la Ciudad de México. La Ciudad de México tuvo un desarrollo altamente competitivo, que ha sido también el catalizador de un largo y sostenido crecimiento urbano. Con el pasar del tiempo, la capital ha sobrepasado las expectativas de los más visionarios. El estudio detallado del asentamiento de Tacubaya (el cual conforma una parte dinámica de la Ciudad de México), permitirá al lector evaluar el extravagante crecimiento que ocurre en la Ciudad de México y los asentamientos que lo rodean, en la primera mitad del siglo XX. Tacubaya, así como muchos de los pequeños poblados preexistentes que se ubicaban en las afueras de la gran urbe, fue alcanzado y engullido por la mancha urbana, sufriendo importantes cambios en su núcleo urbano. Sin embargo, partes de esta antigua centralidad han persistido junto con una parte de los elementos urbanos que la estructuraban; monumentos y riquezas históricas, los cuales han facilitado la reinvención de su centro urbano, sobreviviendo tanto a los abates del tiempo como a las oleadas de nuevos pobladores. El lugar que permanece es un centro urbano sumamente fragmentado, permeado por: una incesante superposición de tejidos y elementos estructuradores olvidados, poblaciones flotantes y de paso que desestabilizan las zonas residenciales, estratos sociales cada vez más apartados. Pensaríamos que las circunstancias que envuelven la demarcación la han dejado en caos, sin embargo, para la sorpresa de muchos, Tacubaya se sigue adaptando a pesar de todos los obstáculos. ABSTRACT In urbanism, the type of spatial fragmentation, that will be the main focus of this Thesis, occurs when a stronger and denser environment takes over a smaller entity, forcing it to adapt its functional relations. This type of fragmentation will be analyzed taking into account three specific factors (speculation, disorganization, and lack of protection) that mold the development of modern urbanistic processes in large Latin American cities, particularly in Mexico City. Mexico City had a highly competitive and bright development, which served as catalyst in a long and sustained urban growth. With the passing of time, the capital has outgrown the measures, previsions and administrative limits created by the government and its visionaries. The detailed study of the Tacubaya settlement (which conforms a vibrant part of Mexico City) will allow the reader to appreciate the exceptional and rare growth that occurs in Mexico City and in the settlements that surround it, in the first half of the 20th century. Tacubaya as well as many other small preexisting settlements located on the outskirts of the city, has been engulfed by the urban expansion suffering important changes in its urban core. Parts of the ancient centrality have persisted along with its structural urban elements, due mainly to monuments and other historical entities that have facilitated the reinvention of the downtown area, helping it survive not only the passing of time, but also the incrementing population. The city that now exists is fragmented beyond recognition. Tacubaya is permeated by an endless fabric overlay created by forgotten structural elements, floating populations that affect the residential zones, and a polarized society that diverges with every passing day. We may think that the circumstances that surround the city have left it in shambles; however, to the surprise of many, Tacubaya is still adapting in spite of all the obstacles.

Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

Los tipos de datos concurrentes son implementaciones concurrentes de las abstracciones de datos clásicas, con la diferencia de que han sido específicamente diseñados para aprovechar el gran paralelismo disponible en las modernas arquitecturas multiprocesador y multinúcleo. La correcta manipulación de los tipos de datos concurrentes resulta esencial para demostrar la completa corrección de los sistemas de software que los utilizan. Una de las mayores dificultades a la hora de diseñar y verificar tipos de datos concurrentes surge de la necesidad de tener que razonar acerca de un número arbitrario de procesos que invocan estos tipos de datos de manera concurrente. Esto requiere considerar sistemas parametrizados. En este trabajo estudiamos la verificación formal de propiedades temporales de sistemas concurrentes parametrizados, poniendo especial énfasis en programas que manipulan estructuras de datos concurrentes. La principal dificultad a la hora de razonar acerca de sistemas concurrentes parametrizados proviene de la interacción entre el gran nivel de concurrencia que éstos poseen y la necesidad de razonar al mismo tiempo acerca de la memoria dinámica. La verificación de sistemas parametrizados resulta en sí un problema desafiante debido a que requiere razonar acerca de estructuras de datos complejas que son accedidas y modificadas por un numero ilimitado de procesos que manipulan de manera simultánea el contenido de la memoria dinámica empleando métodos de sincronización poco estructurados. En este trabajo, presentamos un marco formal basado en métodos deductivos capaz de ocuparse de la verificación de propiedades de safety y liveness de sistemas concurrentes parametrizados que manejan estructuras de datos complejas. Nuestro marco formal incluye reglas de prueba y técnicas especialmente adaptadas para sistemas parametrizados, las cuales trabajan en colaboración con procedimientos de decisión especialmente diseñados para analizar complejas estructuras de datos concurrentes. Un aspecto novedoso de nuestro marco formal es que efectúa una clara diferenciación entre el análisis del flujo de control del programa y el análisis de los datos que se manejan. El flujo de control del programa se analiza utilizando reglas de prueba y técnicas de verificación deductivas especialmente diseñadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, nuestras técnicas deductivas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Las condiciones de verificación generadas se corresponden con los datos manipulados. Estudiamos el diseño de procedimientos de decisión especializados capaces de lidiar con estas condiciones de verificación de manera completamente automática. Investigamos teorías decidibles capaces de describir propiedades de tipos de datos complejos que manipulan punteros, tales como implementaciones imperativas de pilas, colas, listas y skiplists. Para cada una de estas teorías presentamos un procedimiento de decisión y una implementación práctica construida sobre SMT solvers. Estos procedimientos de decisión son finalmente utilizados para verificar de manera automática las condiciones de verificación generadas por nuestras técnicas de verificación parametrizada. Para concluir, demostramos como utilizando nuestro marco formal es posible probar no solo propiedades de safety sino además de liveness en algunas versiones de protocolos de exclusión mutua y programas que manipulan estructuras de datos concurrentes. El enfoque que presentamos en este trabajo resulta ser muy general y puede ser aplicado para verificar un amplio rango de tipos de datos concurrentes similares. Abstract Concurrent data types are concurrent implementations of classical data abstractions, specifically designed to exploit the great deal of parallelism available in modern multiprocessor and multi-core architectures. The correct manipulation of concurrent data types is essential for the overall correctness of the software system built using them. A major difficulty in designing and verifying concurrent data types arises by the need to reason about any number of threads invoking the data type simultaneously, which requires considering parametrized systems. In this work we study the formal verification of temporal properties of parametrized concurrent systems, with a special focus on programs that manipulate concurrent data structures. The main difficulty to reason about concurrent parametrized systems comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. This parametrized verification problem is very challenging, because it requires to reason about complex concurrent data structures being accessed and modified by threads which simultaneously manipulate the heap using unstructured synchronization methods. In this work, we present a formal framework based on deductive methods which is capable of dealing with the verification of safety and liveness properties of concurrent parametrized systems that manipulate complex data structures. Our framework includes special proof rules and techniques adapted for parametrized systems which work in collaboration with specialized decision procedures for complex data structures. A novel aspect of our framework is that it cleanly differentiates the analysis of the program control flow from the analysis of the data being manipulated. The program control flow is analyzed using deductive proof rules and verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, our techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. The verification conditions correspond to the data manipulation. We study the design of specialized decision procedures to deal with these verification conditions fully automatically. We investigate decidable theories capable of describing rich properties of complex pointer based data types such as stacks, queues, lists and skiplists. For each of these theories we present a decision procedure, and its practical implementation on top of existing SMT solvers. These decision procedures are ultimately used for automatically verifying the verification conditions generated by our specialized parametrized verification techniques. Finally, we show how using our framework it is possible to prove not only safety but also liveness properties of concurrent versions of some mutual exclusion protocols and programs that manipulate concurrent data structures. The approach we present in this work is very general, and can be applied to verify a wide range of similar concurrent data types.

Garantía de calidad en Educación Virtual No Formal para Pueblos Indígenas

Este trabajo de investigación presenta un modelo de garantía de calidad en educación Alternativa en modalidad virtual para Pueblos Indígenas del departamento de La Paz, Bolivia. Se plantea el modelo teórico constituido por componentes que emergen de la problemática enunciada, complementado con un análisis comparativo de modelos de calidad en educación virtual y la selección de variables e indicadores. Se da también una descripción del modelo causal explicativo inicial, todo esto utilizando elementos adecuados a las características de Pueblos indígenas del Dpto. de La Paz. Más adelante, se detalla la experiencia de capacitación en TIC’s a dos poblaciones indígenas aplicando el modelo planteado, lo que ha permitido hacer una validación empírica de este. Asimismo, se da a conocer los resultados que arrojaron las encuestas de calidad provenientes de la aplicación del modelo y el llenado correspondiente de las mismas. A partir de estos datos se ha realizado los análisis estadísticos pertinentes para una validación formal del modelo, estructurando una base de datos con la que se logra validar el modelo a través del análisis confirmatorio que conduce a verificar el ajuste de los datos muestrales con el modelo propuesto. ABSTRACT This research presents a model of quality assurance in Alternative education in virtual mode for indigenous communities in the department of La Paz, Bolivia. The theoretical model consisting of components that emerge from the problem expressed, supplemented by a comparative analysis of quality models in virtual education and the selection of variables and indicators arise. It also gives a description of the initial causal explanatory model, all using suited to the characteristics of indigenous communities in the Department of La Paz. Later, the experience of ICT training in two indigenous peoples applying the detailed proposed model, which has allowed for an empirical validation of this. It also discloses the results yielded quality surveys from the application of the model and the corresponding filling them. From these data it was performed statistical analysis relevant to a formal model validation, structuring a database with that achieved validate the model through confirmatory analysis leading to check the setting of the sample data with the model proposed.

Configuración formal de los rosetones románicos de la ciudad de Zamora

La presente tesis estudia los rosetones románicos de la ciudad de Zamora. La elección del tema tiene como objetivo profundizar en el conocimiento de estos elementos ya que la información existente sobre ellos es muy escasa. El análisis de estos rosetones se ha realizado desde una perspectiva globalizadora que abarca aspectos tales como los geográficos, morfológicos, funcionales, compositivos, constructivos, geométricos, ornamentales, otros. Así mismo, para el desarrollo de esta investigación se ha considerado necesario el estudio de temas históricos, estilísticos, simbólicos, religiosos, culturales, etc., que aportan el marco contextual que permiten su mejor entendimiento. El estudio de cada rosetón ha permitido implementar y desarrollar un método de trabajo analítico basado en el estudio particular de una serie de aspectos como los anteriormente mencionados, así como plantear una estrategia que permite la reconstitución gráfica de los rosetones, basándose en un sistema de módulos que facilitan trabajar de acuerdo a las proporciones de los elementos; hecho que permite acercarnos con gran exactitud a la representación del objeto real cuando se carece de medidas. El desarrollo de esta investigación ha llevado a establecer entre otras cosas que la definición de “ventana circular” que se le atribuye a los rosetones románicos no es acertada, puesto que la función que cumplen en el edificio religioso es más bien de carácter simbólico. ABSTRACT This thesis studies the Romanesque rose windows of the Zamora city. The choice of topic is intended to deepen the knowledge of these elements as the existing information about them is very scarce. The analysis of these rose windows was made from a global perspective covering aspects such as geographic, morphological, functional, compositional, construction, geometric, ornamental, other. Also, for the development of this research it was considered necessary to study historical, stylistic, symbolic, religious, cultural issues, etc., that provide the contextual framework that allow for better understanding. The study of each rose windows has allowed implement and develop a method of analytical work based on the particular study a number of issues such as those mentioned above, as well as devise a strategy that allows the graphic reconstitution of the rose windows, based on a system of modules facilitate work according to the proportions of the elements; made with great precision approach allows the representation of the real thing when it lacks measures. The development of this research has led to establish among other things that the definition of "circular window" that is attributed to the Romanesque rose windows is not successful because the role in the religious building is rather symbolic.

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.