In this thesis, an adaptive transit routing (ATR) problem in a schedule based stochastic time-dependent transit network is defined and formulated as a finite horizon Markov Decision Process (MDP). The transit link travel times are assumed to be random with known probability distributions. Routing strategies are defined to be conditional on the arrival times at intermediate nodes, and the location and arrival times of other buses in the network. In other words, a traveler in the network decides to walk, wait or board a bus based on the real time information of all buses in the network. The objective is to find a strategy that minimizes the expected travel time, subject to constraints that guarantee that the destination is reached within a certain threshold. The value of the threshold was chosen to reflect the risk averse attitude of travelers and is computed based on the earliest time by which the destination can be reached with probability 1. The problem inherits the curse of dimensionality and state space reduction through pre-processing is achieved by solving variants of the time dependent shortest path problem. An interesting analogy between the state space reduction techniques and the concept of light cones is discussed. A dynamic program framework to solve the problem is developed by defining the state space, decision space and transition functions. Numerical results on a small instance of the Austin transit network are presented to investigate the extent of reduction in state space using the proposed methods. / text

The challenge this thesis addresses is to speed up the development of concurrent programs by increasing the efficiency with which concurrent programs can be tested and consequently evolved. The goal of this thesis is to generate methods and tools that help software engineers increase confidence in the correct operation of their programs. To achieve this goal, this thesis advocates testing of concurrent software using a systematic approach capable of enumerating possible executions of a concurrent program. The practicality of the systematic testing approach is demonstrated by presenting a novel software infrastructure that repeatedly executes a program test, controlling the order in which concurrent events happen so that different behaviors can be explored across different test executions. By doing so, systematic testing circumvents the limitations of traditional ad-hoc testing, which relies on chance to discover concurrency errors. However, the idea of systematic testing alone does not quite solve the problem of concurrent software testing. The combinatorial nature of the number of ways in which concurrent events of a program can execute causes an explosion of the number of possible interleavings of these events, a problem referred to as state space explosion. To address the state space explosion problem, this thesis studies techniques for quantifying the extent of state space explosion and explores several directions for mitigating state space explosion: parallel state space exploration, restricted runtime scheduling, and abstraction reduction. In the course of its research exploration, this thesis pushes the practical limits of systematic testing by orders of magnitude, scaling systematic testing to real-world programs of unprecedented complexity.

Existem vários problemas clássicos na área de pesquisa operacional que trabalham com o tema vinculado à designação de veículos em um sistema logístico, entre eles o Problema de Escalonamento de Veículos com Múltiplas Garagens (MDVSP). Esses modelos são largamente utilizados e representam uma das etapas essenciais para o planejamento de trânsito em massa (HAGHANI e BANIHASHEMI, 2002). Tratando-se de sistemas logísticos reais, dificilmente encontra-se um ambiente onde os veículos devem partir e chegar a uma única garagem, por isso torna-se necessário o planejamento das seqüências de viagens de modo a reduzir os custos de deslocamentos com o aproveitamento das múltiplas garagens distribuídas geograficamente. Infelizmente, considerando a complexidade exponencial do MDVSP, muitas vezes sua aplicação torna-se inviável na solução de problemas reais. Por essa razão, poucos trabalhos abordam o MDVSP de modo a conseguir solucionar o problema para uma grande quantidade de viagens e garagens. A maioria das pesquisas trabalha com instâncias inferiores a 500 viagens e quatro garagens, mostrando-se pouco aplicáveis. Esse estudo refere-se a um trabalho de pesquisa operacional que aborda soluções de problemas de escalonamento de veículos com múltiplas garagens (MDVSP) considerando sua aplicabilidade em sistemas reais. Tendo em vista a complexidade exponencial do MDVSP, nesse estudo optou-se por tratar o problema através de uma abordagem baseada na redução do espaço de estados e na utilização de heurísticas. Durante essa pesquisa três procedimentos de redução do espaço de estados foram adotados. Os resultados apontam que é possível reduzir em até 98% o número de variáveis nesses problemas sem comprometer uma solução satisfatória ou ótima. Além dos procedimentos de redução do espaço de estados, foi desenvolvido um procedimento de buscar a solução do MDVSP. Através desse último procedimento foi possível resolver o MDVSP com até 3000 viagens e oito garagens. Sendo assim, nesse estudo desenvolveram-se modelos que servem para o planejamento de um sistema logístico através da aplicação de cenários, com vistas a permitir a geração e análise de alternativas de escalonamento. Objetivou-se com isso, fornecer ao sistema logístico um modelo amplo que permita a escolha da ação mais conveniente e eficiente a ser tomada em modelos compostos por diversas garagens. / There are many classics problems in operations research concerning optimal assignment vehicles in logistical system. The multiple depot vehicle scheduling problem (MDVSP) is one of them. This problem is largely used to represent and solve mass transit planning (HAGHANI e BANIHASHEMI, 2002). Considering a real logistical system, it is very difficult to find out a situation where the vehicles must leave and come to only one depot. In general, the shipping company has several depots located at different sites in a network. In this way, it is strongly necessary to reduce cost through the planning of sequence trips taking into account multiple depots geographically distributed. Unfortunately, the exponential complexity of the MDVSP reduces, in the most cases, the applicability of this problem in the real world. For this reason, few researchers address the MDVSP to solve real world problems considering a large number of trips and depots. The majority of the research dealing with the MDVSP works with instances lower than 500 trips and four depots, what can be considered a major constraint for its practical use. The main objective of this work is to solve the MDVSP for very large instances. A state space reduction approach combined with heuristic procedures are developed to obtain a realistic way of solving this complex problem. In this research, three state space reduction procedures were developed. The results appointed that is possible to reduce until 98% of variables in the MDVSP without jeopardizing an optimal solution. Furthermore, heuristic procedures were developed to obtain solutions without relaxing any realworld constraint of the problem. The solution procedure developed was compared with wellknown available instances. The method is able to solve the MDVSP with 3000 trips and eight depots in less than 11 minutes. Although the solution process does not obtain the best solution in all tested instances, it is by far the quickest.

Existem vários problemas clássicos na área de pesquisa operacional que trabalham com o tema vinculado à designação de veículos em um sistema logístico, entre eles o Problema de Escalonamento de Veículos com Múltiplas Garagens (MDVSP). Esses modelos são largamente utilizados e representam uma das etapas essenciais para o planejamento de trânsito em massa (HAGHANI e BANIHASHEMI, 2002). Tratando-se de sistemas logísticos reais, dificilmente encontra-se um ambiente onde os veículos devem partir e chegar a uma única garagem, por isso torna-se necessário o planejamento das seqüências de viagens de modo a reduzir os custos de deslocamentos com o aproveitamento das múltiplas garagens distribuídas geograficamente. Infelizmente, considerando a complexidade exponencial do MDVSP, muitas vezes sua aplicação torna-se inviável na solução de problemas reais. Por essa razão, poucos trabalhos abordam o MDVSP de modo a conseguir solucionar o problema para uma grande quantidade de viagens e garagens. A maioria das pesquisas trabalha com instâncias inferiores a 500 viagens e quatro garagens, mostrando-se pouco aplicáveis. Esse estudo refere-se a um trabalho de pesquisa operacional que aborda soluções de problemas de escalonamento de veículos com múltiplas garagens (MDVSP) considerando sua aplicabilidade em sistemas reais. Tendo em vista a complexidade exponencial do MDVSP, nesse estudo optou-se por tratar o problema através de uma abordagem baseada na redução do espaço de estados e na utilização de heurísticas. Durante essa pesquisa três procedimentos de redução do espaço de estados foram adotados. Os resultados apontam que é possível reduzir em até 98% o número de variáveis nesses problemas sem comprometer uma solução satisfatória ou ótima. Além dos procedimentos de redução do espaço de estados, foi desenvolvido um procedimento de buscar a solução do MDVSP. Através desse último procedimento foi possível resolver o MDVSP com até 3000 viagens e oito garagens. Sendo assim, nesse estudo desenvolveram-se modelos que servem para o planejamento de um sistema logístico através da aplicação de cenários, com vistas a permitir a geração e análise de alternativas de escalonamento. Objetivou-se com isso, fornecer ao sistema logístico um modelo amplo que permita a escolha da ação mais conveniente e eficiente a ser tomada em modelos compostos por diversas garagens. / There are many classics problems in operations research concerning optimal assignment vehicles in logistical system. The multiple depot vehicle scheduling problem (MDVSP) is one of them. This problem is largely used to represent and solve mass transit planning (HAGHANI e BANIHASHEMI, 2002). Considering a real logistical system, it is very difficult to find out a situation where the vehicles must leave and come to only one depot. In general, the shipping company has several depots located at different sites in a network. In this way, it is strongly necessary to reduce cost through the planning of sequence trips taking into account multiple depots geographically distributed. Unfortunately, the exponential complexity of the MDVSP reduces, in the most cases, the applicability of this problem in the real world. For this reason, few researchers address the MDVSP to solve real world problems considering a large number of trips and depots. The majority of the research dealing with the MDVSP works with instances lower than 500 trips and four depots, what can be considered a major constraint for its practical use. The main objective of this work is to solve the MDVSP for very large instances. A state space reduction approach combined with heuristic procedures are developed to obtain a realistic way of solving this complex problem. In this research, three state space reduction procedures were developed. The results appointed that is possible to reduce until 98% of variables in the MDVSP without jeopardizing an optimal solution. Furthermore, heuristic procedures were developed to obtain solutions without relaxing any realworld constraint of the problem. The solution procedure developed was compared with wellknown available instances. The method is able to solve the MDVSP with 3000 trips and eight depots in less than 11 minutes. Although the solution process does not obtain the best solution in all tested instances, it is by far the quickest.

Existem vários problemas clássicos na área de pesquisa operacional que trabalham com o tema vinculado à designação de veículos em um sistema logístico, entre eles o Problema de Escalonamento de Veículos com Múltiplas Garagens (MDVSP). Esses modelos são largamente utilizados e representam uma das etapas essenciais para o planejamento de trânsito em massa (HAGHANI e BANIHASHEMI, 2002). Tratando-se de sistemas logísticos reais, dificilmente encontra-se um ambiente onde os veículos devem partir e chegar a uma única garagem, por isso torna-se necessário o planejamento das seqüências de viagens de modo a reduzir os custos de deslocamentos com o aproveitamento das múltiplas garagens distribuídas geograficamente. Infelizmente, considerando a complexidade exponencial do MDVSP, muitas vezes sua aplicação torna-se inviável na solução de problemas reais. Por essa razão, poucos trabalhos abordam o MDVSP de modo a conseguir solucionar o problema para uma grande quantidade de viagens e garagens. A maioria das pesquisas trabalha com instâncias inferiores a 500 viagens e quatro garagens, mostrando-se pouco aplicáveis. Esse estudo refere-se a um trabalho de pesquisa operacional que aborda soluções de problemas de escalonamento de veículos com múltiplas garagens (MDVSP) considerando sua aplicabilidade em sistemas reais. Tendo em vista a complexidade exponencial do MDVSP, nesse estudo optou-se por tratar o problema através de uma abordagem baseada na redução do espaço de estados e na utilização de heurísticas. Durante essa pesquisa três procedimentos de redução do espaço de estados foram adotados. Os resultados apontam que é possível reduzir em até 98% o número de variáveis nesses problemas sem comprometer uma solução satisfatória ou ótima. Além dos procedimentos de redução do espaço de estados, foi desenvolvido um procedimento de buscar a solução do MDVSP. Através desse último procedimento foi possível resolver o MDVSP com até 3000 viagens e oito garagens. Sendo assim, nesse estudo desenvolveram-se modelos que servem para o planejamento de um sistema logístico através da aplicação de cenários, com vistas a permitir a geração e análise de alternativas de escalonamento. Objetivou-se com isso, fornecer ao sistema logístico um modelo amplo que permita a escolha da ação mais conveniente e eficiente a ser tomada em modelos compostos por diversas garagens. / There are many classics problems in operations research concerning optimal assignment vehicles in logistical system. The multiple depot vehicle scheduling problem (MDVSP) is one of them. This problem is largely used to represent and solve mass transit planning (HAGHANI e BANIHASHEMI, 2002). Considering a real logistical system, it is very difficult to find out a situation where the vehicles must leave and come to only one depot. In general, the shipping company has several depots located at different sites in a network. In this way, it is strongly necessary to reduce cost through the planning of sequence trips taking into account multiple depots geographically distributed. Unfortunately, the exponential complexity of the MDVSP reduces, in the most cases, the applicability of this problem in the real world. For this reason, few researchers address the MDVSP to solve real world problems considering a large number of trips and depots. The majority of the research dealing with the MDVSP works with instances lower than 500 trips and four depots, what can be considered a major constraint for its practical use. The main objective of this work is to solve the MDVSP for very large instances. A state space reduction approach combined with heuristic procedures are developed to obtain a realistic way of solving this complex problem. In this research, three state space reduction procedures were developed. The results appointed that is possible to reduce until 98% of variables in the MDVSP without jeopardizing an optimal solution. Furthermore, heuristic procedures were developed to obtain solutions without relaxing any realworld constraint of the problem. The solution procedure developed was compared with wellknown available instances. The method is able to solve the MDVSP with 3000 trips and eight depots in less than 11 minutes. Although the solution process does not obtain the best solution in all tested instances, it is by far the quickest.

Avec l'évolution des technologies, la complexité des systèmes informatiques ne cesse de s'accroître. Parmi ces systèmes, on retrouve les logiciels critiques qui doivent offrir une garantie de sûreté de fonctionnement qui s'avère crucial et pour lesquels un dysfonctionnement peut avoir des conséquences graves. Les méthodes formelles fournissent des outils permettant de garantir mathématiquement l'absence de certaines erreurs. Ces méthodes sont indispensables pour assurer les plus hauts niveaux de sûreté. Mais l'application de ces méthodes sur un code système bas niveau se heurte à des difficultés d'ordre pratique et théorique. Les principales difficultés concernent la prise en compte des aspects bas niveau, comme les pointeurs et les interactions avec le matériel spécifique. De plus, le fait que ces systèmes soient concurrents conduit à une augmentation exponentielle du nombre de comportements possibles, ce qui rend plus difficile leur vérification. Dans cette thèse, nous proposons une méthodologie pour la spécification et la vérification par model-checking de ce type de systèmes, en particulier, ceux implémentés en C. Cette méthodologie est basée sur la traduction de la sémantique de C en TLA+, un langage de spécification formel adapté à la modélisation de systèmes concurrents. Nous avons proposé un modèle de mémoire et d'exécution d'un programme C séquentiel en TLA+. En se basant sur ce modèle, nous avons proposé un ensemble de règles de traduction d'un code C en TLA+ que nous avons implémenté dans un outil, appelé C2TLA+. Nous avons montré comment ce modèle peut s'étendre pour modéliser les programmes C concurrents et gérer la synchronisation entre plusieurs processus ainsi que leur ordonnancement. Pour réduire la complexité du model-checking, nous avons proposé une technique permettant de réduire significativement la complexité de la vérification. Cette réduction consiste pour un code C à agglomérer une suite d'instructions lors de la génération du code TLA+, sous réserve d'un ensemble de conditions.Nous avons appliqué la méthodologie proposée dans cette thèse sur un cas d'étude réel issu de l'implémentation d'un micronoyau industriel,sur lequel nous avons vérifié un ensemble de propriétés fonctionnelles. L'application de la réduction a permis de réduire considérablement le temps de la vérification, ce qui la rend utilisable en pratique.Les résultats ont permis d'étudier le comportement du système, de vérifier certaines propriétés et de trouver des bugs indétectables par des simples tests. / Software systems are critical and complex. In order to guarantee their correctness, the use of formal methodsis important. These methods can be defined as mathematically based techniques, languages and tools for specifying and reasoning about systems. But, the application of formal methods to software systems, implemented in C, is challenging due to the presence of pointers, pointer arithmetic andinteraction with hardware. Moreover, software systems are often concurrent, making the verification process infeasible. This work provides a methodology to specify and verify C software systems usingmodel-checking technique. The proposed methodology is based on translating the semantics of Cinto TLA+, a formal specification language for reasoning about concurrent and reactive systems. We define a memory and execution model for a sequential program and a set of translation rules from C to TLA+ that we developed in a tool called C2TLA+. Based on this model, we show that it can be extended to support concurrency, synchronization primitives and process scheduling. Although model-checking is an efficient and automatic technique, it faces the state explosion problem when the system becomes large. To overcome this problem, we propose a state-space reduction technique. The latter is based on agglomerating a set of C instructions during the generation phase of the TLA+ specification. This methodology has been applied to a concrete case study, a microkernel of an industrial real-time operating system, on which a set of functional properties has been verified. The application of the agglomeration technique to the case study shows the usefulness of the proposed technique in reducing the complexity of verification. The obtained results allow us to study the behavior of the system and to find errors undetectable using traditional testing techniques.

The area of formal analysis of cryptographic protocols has been an active one since the mid 80’s. The idea is to verify communication protocols that use encryption to guarantee secrecy and that use authentication of data to ensure security. Formal methods are used in protocol analysis to provide formal proofs of security, and to uncover bugs and security flaws that in some cases had remained unknown long after the original protocol publication, such as the case of the well known Needham-Schroeder Public Key (NSPK) protocol. In this thesis we tackle problems regarding the three main pillars of protocol verification: modelling capabilities, verifiable properties, and efficiency. This thesis is devoted to investigate advanced features in the analysis of cryptographic protocols tailored to the Maude-NPA tool. This tool is a model-checker for cryptographic protocol analysis that allows for the incorporation of different equational theories and operates in the unbounded session model without the use of data or control abstraction. An important contribution of this thesis is relative to theoretical aspects of protocol verification in Maude-NPA. First, we define a forwards operational semantics, using rewriting logic as the theoretical framework and the Maude programming language as tool support. This is the first time that a forwards rewriting-based semantics is given for Maude-NPA. Second, we also study the problem that arises in cryptographic protocol analysis when it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the protocol equational theory. We also study techniques to extend Maude-NPA capabilities to support the verification of a wider class of protocols and security properties. First, we present a framework to specify and verify sequential protocol compositions in which one or more child protocols make use of information obtained from running a parent protocol. Second, we present a theoretical framework to specify and verify protocol indistinguishability in Maude-NPA. This kind of properties aim to verify that an attacker cannot distinguish between two versions of a protocol: for example, one using one secret and one using another, as it happens in electronic voting protocols. Finally, this thesis contributes to improve the efficiency of protocol verification in Maude-NPA. We define several techniques which drastically reduce the state space, and can often yield a finite state space, so that whether the desired security property holds or not can in fact be decided automatically, in spite of the general undecidability of such problems. / Santiago Pinazo, S. (2015). Advanced Features in Protocol Verification: Theory, Properties, and Efficiency in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/48527

Tesis por compendio / [ES] La herramienta criptográfica Maude-NPA es un verificador de modelos especializado para protocolos de seguridad criptográficos que tienen en cuenta las propiedades algebraicas de un sistema criptográfico. En la literatura, las propiedades criptográficas adicionales han descubierto debilidades de los protocolos de seguridad y, en otros casos, son parte de los supuestos de seguridad del protocolo para funcionar correctamente. Maude-NPA tiene una base teórica en la rewriting logic, la unificación ecuacional y el narrowing para realizar una búsqueda hacia atrás desde un patrón de estado inseguro para determinar si es alcanzable o no. Maude-NPA se puede utilizar para razonar sobre una amplia gama de propiedades criptográficas, incluida la cancelación del cifrado y descifrado, la exponenciación de Diffie-Hellman, el exclusive-or y algunas aproximaciones del cifrado homomórfico. En esta tesis consideramos nuevas propiedades criptográficas, ya sea como parte de protocolos de seguridad o para descubrir nuevos ataques. También hemos modelado diferentes familias de protocolos de seguridad, incluidos los Distance Bounding Protocols or Multi-party key agreement protocolos. Y hemos desarrollado nuevas técnicas de modelado para reducir el coste del análisis en protocolos con tiempo y espacio. Esta tesis contribuye de varias maneras al área de análisis de protocolos criptográficos y muchas de las contribuciones de esta tesis pueden ser útiles para otras herramientas de análisis criptográfico. / [CA] L'eina criptografica Maude-NPA es un verificador de models especialitzats per a protocols de seguretat criptogràfics que tenen en compte les propietats algebraiques d'un sistema criptogràfic. A la literatura, les propietats criptogràfiques addicionals han descobert debilitats dels protocols de seguretat i, en altres casos, formen part dels supòsits de seguretat del protocol per funcionar correctament. Maude-NPA te' una base teòrica a la rewriting lògic, la unificació' equacional i narrowing per realitzar una cerca cap enrere des d'un patró' d'estat insegur per determinar si es accessible o no. Maude-NPA es pot utilitzar per raonar sobre una amplia gamma de propietats criptogràfiques, inclosa la cancel·lació' del xifratge i desxifrat, l'exponenciacio' de Diffie-Hellman, el exclusive-or i algunes aproximacions del xifratge homomòrfic. En aquesta tesi, considerem noves propietats criptogràfiques, ja sigui com a part de protocols de seguretat o per descobrir nous atacs. Tambe' hem modelat diferents famílies de protocols de seguretat, inclosos els Distance Bounding Protocols o Multi-party key agreement protocols. I hem desenvolupat noves tècniques de modelització' de protocols per reduir el cost de l'analisi en protocols amb temps i espai. Aquesta tesi contribueix de diverses maneres a l’àrea de l’anàlisi de protocols criptogràfics i moltes de les contribucions d’aquesta tesi poden ser útils per a altres eines d’anàlisi criptogràfic. / [EN] The Maude-NPA crypto tool is a specialized model checker for cryptographic security protocols that take into account the algebraic properties of the cryptosystem. In the literature, additional crypto properties have uncovered weaknesses of security protocols and, in other cases, they are part of the protocol security assumptions in order to function properly. Maude-NPA has a theoretical basis on rewriting logic, equational unification, and narrowing to perform a backwards search from an insecure state pattern to determine whether or not it is reachable. Maude-NPA can be used to reason about a wide range of cryptographic properties, including cancellation of encryption and decryption, Diffie-Hellman exponentiation, exclusive-or, and some approximations of homomorphic encryption. In this thesis, we consider new cryptographic properties, either as part of security protocols or to discover new attacks. We have also modeled different families of security protocols, including Distance Bounding Protocols or Multi-party key agreement protocols. And we have developed new protocol modeling techniques to reduce the time and space analysis effort. This thesis contributes in several ways to the area of cryptographic protocol analysis and many of the contributions of this thesis can be useful for other crypto analysis tools. / This thesis would not have been possible without the funding of a set of research projects. The main contributions and derivative works of this thesis have been made in the context of the following projects: - Ministry of Economy and Business of Spain : Project LoBaSS Effective Solutions Based on Logic, Scientific Research under award number TIN2015-69175-C4-1-R, this project was focused on using powerful logic-based technologies to analyze safety-critical systems. - Air Force Office of Scientific Research of United States of America : Project Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA Scientific Research under award number FA9550-17-1-0286 - State Investigation Agency of Spain : Project FREETech: Formal Reasoning for Enabling and Emerging Technologies Scientific I+D-i Research under award number RTI2018-094403-B-C32 / Aparicio Sánchez, D. (2022). Modeling and Analysis of Advanced Cryptographic Primitives and Security Protocols in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/190915 / Compendio