La tesi presenta una nova teoria i una metodologia per a la verificació formal de propietats de seguretat en sistemes temporitzats. El correcte funcionament d'aquests sistemes no només depèn d'un conjunt de propietats funcionals, sinó també de certes suposicions sobre els retards dels components del sistema i els temps de resposta de l'entorn en el que opera el sistema. La verificació d'aquest tipus de sistemes típicament implica la resolució de varis problemes computacionalment molt complexes. En concret, la explosió combinatòria d'estats es fa especialment palesa en incloure la dimensió temporal en el problema.La teoria en que es fonamenta el mètode de verificació proposat estén els mètodes simbòlics convencionals basats en BDDs, per al seu ús en la verificació de sistemes temporitzats modelats usant sistemes de transicions temporitzats. La teoria es basa en el paradigma de les relacions temporals relatives, que enlloc de considerar els temps exactes d'ocurrència dels esdeveniments, considera l'efecte dels retards en termes d'ordenacions relatives entre esdeveniments. Per exemple, per garantir que una carrera no se propaga en un circuit digital, sovint és suficient comprovar que cert senyal commuta abans que un altre, enlloc d'identificar exactament els instants en que ambdós senyals commuten. Fins i tot, no és necessari calcular la informació temporal per al sistema complet en el seu conjunt, enlloc d'això es pot calcular localment per a la part del sistema relacionada amb la demostració d'una determinada propietat. Això és possible gràcies a una observació crucial:que el conjunt d'execucions d'un sistema de transicions es pot cobrir mitjançant un conjunt d'ordres parcials. En conseqüència, per demostrar una propietat només és necessari considerar un subconjunt dels esdeveniments del sistema i l'anàlisi temporal pot fer-se de forma molt eficient.Els mètodes convencionals per a la verificació de sistemes temporitzats es basen en el càlcul exacte de l'espai d'estats temporitzat del sistema com a primer pas de l'anàlisi. Tot i que s'han proposat tècniques eficients per a mitigar la complexitat associada, els mètodes d'anàlisi simbòlic no són fàcilment aplicables. Conseqüentment, el problema de l'explosió combinatòria de l'espai d'estats temporitzat sovint limita la aplicació pràctica dels mètodes esmentats a sistemes de tamany moderat.Per altra banda, el mètode proposat a la tesi es basa en un refinament incremental de l'espai d'estats no temporitzat del sistema, de forma que la informació temporal només s'incorpora al sistema quan aquesta es fa necessària. La informació temporal es deriva a partir d'una anàlisi temporal eficient sobre petits conjunts d'esdeveniments. L'espai d'estats refinat es captura sota el model dels sistemes de transicions mandrosos, que permeten la representació eficient del domini temporal d'un sistema tot usant tècniques simbòliques convencionals. En conseqüència, el mètode pot aplicar-se potencialment a sistemes de tamany més gran o amb més nivell de detall, que els sistemes que poden verificar-se mitjançant mètodes similars. Addicionalment, el fet que el mètode proposat sigui incremental proporciona una bona forma d'obtenir al menys resultats parcials fins i tot en sistemes pels que un resultat complet de verificació fóra excessivament complex de calcular.Un aspecte clau del mètode de verificació proposat es que no només comprova la correctesa d'un sistema temporitzat. Si el sistema és correcte, la verificació proporciona un conjunt suficient de relacions temporals relatives que ho demostren. Pel contrari, si el sistema és incorrecte, la verificació proporciona una traça d'error com a contraexemple. L'aspecte més interessant de tota aquesta informació és la seva utilitat al llarg del cicle de disseny d'un sistema. Aquest fet permet mitigar la tradicional distància entre la verificació i el disseny, fet que constitueix un altre aspecte diferencial del mètode de verificació proposat envers a altres mètodes de verificació equivalents.El mètode de verificació proposat s'ha implementat completament en una eina de CAV (Verificació Assistida per Computador) anomenada TRANSYT. L'eina permet manipular sistemes jeràrquics i modulars que poden interoperar mitjançant diversos mecanismes de comunicació. TRANSYT ha demostrat la seva funcionalitat i la validesa del mètode de verificació proposat, mitjançant la verificació de diversos circuits asíncrons temporitzats amb més de 10E+6 estats no temporitzats. Els experiments realitzats inclouen la verificació de: descomposicions de portes lògiques complexes en circuits asíncrons casi-independents-de-la-velocitat, circuits de lògica dominó, sistemes amb comportaments basats en polsos, circuits optimitzats per a velocitat mitjançant suposicions temporals, etc. Addicionalment, s'ha combinat el mètode de verificació proposat amb mètodes de verificació composicional per tal d'atacar la verificació de sistemes temporitzats complexes. En aquesta línia, s'han usat tècniques d'abstracció, raonament del tipus suposició-garantia i inducció matemàtica per tal de demostrar la correctesa de l'arquitectura IPCMOS. Aquesta és una arquitectura segmentada i escalable que permet la interconnexió de subsistemes síncrons amb diferents freqüències de rellotge.Gràcies al caire teòric del mètode de verificació proposat, el seu potencial d'aplicació cobreix un rang de sistemes molt més gran que els esmentats anteriorment, com per exemple: circuits de propòsit específic dissenyats a nivell de transistor per tal d'explotar els límits tecnològics i aconseguir un major rendiment, estructures digitals complexes on la sincronització és crucial (e.g. MOS dinàmic), sistemes asíncrons i del tipus GALS (Globalment Asíncron Localment Síncron), sistemes de temps real, etc. / La tesis presenta una nueva teoría y una metodología para la verificación formal de propiedades de seguridad en sistemas temporizados. El correcto funcionamiento de estos sistemas no sólo depende de un conjunto de propiedades funcionales sino también de ciertas suposiciones sobre los retardos de los componentes del sistema y los tiempos de respuesta del entorno en el que opera el sistema. La verificación de este tipo de sistemas típicamente implica la resolución de varios problemas computacionalmente muy complejos. En concreto, la explosión combinatoria de estados se hace especialmente patente al incluir la dimensión temporal en el problema.La teoría en que se sustenta el método de verificación propuesto extiende los métodos simbólicos convencionales basados en BDDs, para su uso en la verificación de sistemas temporizados modelados usando sistemas de transiciones temporizados. La teoría se basa en el paradigma de las relaciones temporales relativas, que en lugar de considerar los tiempos exactos de ocurrencia de los eventos, considera el efecto de los retardos en términos de ordenaciones relativas entre eventos. Por ejemplo, para garantizar que una carrera no se propaga en un circuito digital, a menudo es suficiente comprobar que cierta señal conmuta antes que otra, en lugar de identificar exactamente los instantes en que ambas señales conmutan. Es más, no es necesario computar la información temporal para el sistema completo en su conjunto, si no sólo localmente para la parte del sistema relacionada con la demostración de una determinada propiedad. Esto es posible gracias a una observación crucial: que el conjunto de ejecuciones de un sistema de transiciones puede cubrirse por un conjunto de órdenes parciales. En consecuencia, para la demostración de una propiedad sólo es necesario considerar un subconjunto de los eventos del sistema y el análisis temporal puede hacerse de forma muy eficiente. Los métodos convencionales para la verificación de sistemas temporizados se basan en el cálculo exacto del espacio de estados temporizado del sistema como primer paso del análisis. Aunque se han propuesta técnicas eficientes para paliar la complejidad asociada, los métodos de análisis simbólico no son fácilmente aplicables. Consecuentemente, el problema de la explosión combinatoria del espacio de estados temporizado a menudo limita la aplicación práctica de dichos métodos a sistemas de tamaño moderado.Por el contrario, el método propuesto en la tesis se basa en un refinamiento incremental del espacio de estados no temporizado del sistema, de forma que la información temporal sólo se incorpora al sistema cuando ésta se hace necesaria. Dicha información temporal se deriva a partir de un análisis temporal eficiente sobre pequeños conjuntos de eventos. El espacio de estados refinado se captura bajo el modelo de los sistemas de transiciones perezosos, que permiten la representación eficiente del dominio temporal de un sistema usando técnicas simbólicas convencionales. En consecuencia, el método puede aplicarse potencialmente a sistemas de mayor tamaño o con mayor nivel de detalle, que los sistemas que pueden verificarse con métodos similares. Adicionalmente, la naturaleza incremental del método propuesto proporciona una buena forma de obtener al menos resultados parciales incluso en sistemas para los cuales un resultado completo de verificación seria excesivamente complejo de calcular.Un aspecto clave del método de verificación propuesto es que no sólo comprueba la corrección de un sistema temporizado. Si el sistema es correcto, la verificación proporciona un conjunto suficiente de relaciones temporales relativas que lo demuestran. Por el contrario, si el sistema es incorrecto, la verificación proporciona una traza de error a modo de contraejemplo. El aspecto más interesante de toda esta información es su utilidad a lo largo del ciclo de diseño de un sistema. Este hecho permite mitigar la tradicional distancia entre la verificación y el diseño en sí, lo que constituye otro aspecto diferencial del método de verificación propuesto frente a otros métodos de verificación equivalentes.El método de verificación propuesto se ha implementado completamente en una herramienta de CAV (Verificación Asistida por Computador) llamada TRANSYT. La herramienta permite manipular sistemas jerárquicos y modulares los cuales pueden interoperar mediante varios mecanismos de comunicación. TRANSYT ha demostrado su funcionalidad así como la validez del método de verificación propuesto, mediante la verificación de diversos circuitos asíncronos temporizados con más de 10E+6 estados no temporizados. Los experimentos realizados incluyen la verificación de: descomposiciones de puertas lógicas complejas en circuitos asíncronos casi-independientes-de-la-velocidad, circuitos de lógica dominó, sistemas con comportamientos basados en pulsos, circuitos optimizados para velocidad mediante suposiciones temporales, etc. Adicionalmente, se ha combinado el método de verificación propuesto con métodos de verificación composicional con el fin de atacar la verificación de sistemas temporizados complejos. En esta línea, se han usado técnicas de abstracción, razonamiento del tipo suposición-garantía e inducción matemática para demostrar la corrección de la arquitectura IPCMOS. Ésta es una arquitectura segmentada y escalable que permite la interconexión de subsistemas síncronos con diferentes frecuencias de reloj.Gracias a la naturaleza teórica del método de verificación propuesto, su potencial de aplicación cubre un rango de sistemas mucho mayor a los citados anteriormente, como por ejemplo: circuitos de propósito específico diseñados a nivel de transistor para explotar los límites tecnológicos en pro de un mayor rendimiento, estructuras digitales complejas en las que la sincronización es crucial (e.g. MOS dinámico), sistemas asíncronos y del tipo GALS (Globalmente Asíncrono Localmente Síncrono), sistemas de tiempo real, etc. / The thesis presents a new theory and methodology for the formal verification of safety properties in timed systems. The correct operation of such systems not only depends on a set of functional properties but also on certain assumptions about the delays of the components of the system and the response times of the environment in which the system operates. The verification of this type of systems typically involves several computationally hard problems. In particular, the combinatorial state explosion problem becomes exacerbated by the time dimension.The theory that supports the proposed verification approach extends the conventional BDD-based symbolic methods to the verification of timed systems, modeled by means of timed transition systems. The theory is based on the relative timing paradigm, which instead of considering exact time differences in the occurrence of events, considers the effect of delays in terms of relative orderings between events. For example, in order to guarantee that a race is not propagated in a digital circuit, it is often sufficient to check that certain signal switches before another, instead of identifying the exact instants of time in which both signals switch. Moreover, the timing information does not need to computed for the overall system, but only locally for the part of the system involved in the proof or disproof of a given property. This is possible thanks to a crucial observation, that the set of executions of a transition system can be covered by a set of partial orders. As a consequence, only a subset of the events of the system is involved in the proof of a property and the timing analysis can be carried out very efficiently. Conventional methods for the verification of timed systems rely on the computation of the exact timed state space of the system as the first step of the analysis. Although efficient techniques have been devised to overcome the complexity issue (e.g. difference bound matrices), symbolic methods cannot be easily applied. Thus, the combinatorial time-state explosion problem often limits the applicability of such methods to moderate-size systems. Instead, the approach proposed in the thesis relies on an incremental refinement of the untimed state space of the system, so that timing information is incorporated as soon as it is needed. The timing information is derived by an efficient off-line timing analysis over small sets of events. The refined state space is captured under the model of lazy transition system, which allows an efficient representation of the timed domain using conventional symbolic methods. As a consequence, the approach can be potentially applied to bigger systems or to systems with more level of detail, than those that can be handled by similar methods for the verification of timed systems. Moreover, the incremental nature of the approach provides a good way to obtain at least partial results even on systems for which complete solutions could be too complex to compute. A key feature of the proposed verification approach is that not only proves or disproves the correctness of a timed system. If the system is correct the set of relative timing relations used for the proof are provided. Such relations constitute a set of sufficient timing constraints that guarantee the correctness of the system. On the other hand, if the system is incorrect, a counterexample failure trace is provided. The most important aspect of all this feedback is that it can be used as valuable back-annotation information along the design process.This feature, which allows to bridge the gap between verification and design, constitutes another differential aspect of our verification approach when compared to other equivalent verification methods. The verification approach has been fully implemented in an experimental CAV tool called TRANSYT. The tool can handle hierarchical and distributed modular systems which can inter-operate by a variety of communication mechanisms. TRANSYT has successfully proved its functionality as well as the validity of the overall verification approach, by verifying a number of timed asynchronous circuits with up to more than 10E+6 untimed states.The experiments cover, for example, the verification of: complex-gate decompositions in quasi-speed-independent asynchronous circuits, delay-reset domino circuits, pulse-based systems, circuits optimized for speed using timing assumptions, etc. Additionally, compositional verification methods have been combined with the basic verification approach in order to tackle the size/complexity issues involved in the verification of complex timed systems. Thus, abstractions, assume-guarantee reasoning and mathematical induction have been used to prove the correctness the IPCMOS architecture. It is a scalable pipelined architecture which is aimed to the interconnection of different clock zones in a system. Thanks to the rather theoretical nature of the proposed verification approach, its potential applicability covers a wider range of systems than those cited above, such as: custom transistor-level circuits that exploit the technology limits for performance, complex digital structures where synchronization is a crucial issue (e.g. dynamic MOS), asynchronous and GALS-type systems, real-time systems, etc.

Abstract This dissertation is focused on the study of the prefetching technique applied to the World Wide Web. This technique lies in processing (e.g., downloading) a Web request before the user actually makes it. By doing so, the waiting time perceived by the user can be reduced, which is the main goal of the Web prefetching techniques. The study of the state of the art about Web prefetching showed the heterogeneity that exists in its performance evaluation. This heterogeneity is mainly focused on four issues: i) there was no open framework to simulate and evaluate the already proposed prefetching techniques; ii) no uniform selection of the performance indexes to be maximized, or even their definition; iii) no comparative studies of prediction algorithms taking into account the costs and benefits of web prefetching at the same time; and iv) the evaluation of techniques under very different or few significant workloads. During the research work, we have contributed to homogenizing the evaluation of prefetching performance by developing an open simulation framework that reproduces in detail all the aspects that impact on prefetching performance. In addition, prefetching performance metrics have been analyzed in order to clarify their definition and detect the most meaningful from the user's point of view. We also proposed an evaluation methodology to consider the cost and the benefit of prefetching at the same time. Finally, the importance of using current workloads to evaluate prefetching techniques has been highlighted; otherwise wrong conclusions could be achieved. The potential benefits of each web prefetching architecture were analyzed, finding that collaborative predictors could reduce almost all the latency perceived by users. The first step to develop a collaborative predictor is to make predictions at the server, so this thesis is focused on an architecture with a server-located predictor. The environment conditions that can be found in the web are als / Doménech I De Soria, J. (2007). Evaluation, Analysis and adaptation of web prefetching techniques in current web [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1841 / Palancia

Actualmente, los clústeres de PCs están considerados como una alternativa eficiente a la hora de construir supercomputadores en los que miles de nodos de computación se conectan mediante una red de interconexión. La red de interconexión tiene que ser diseñada cuidadosamente, puesto que tiene una gran influencia sobre las prestaciones globales del sistema. Dos de los principales parámetros de diseño de las redes de interconexión son la topología y el encaminamiento. La topología define la interconexión de los elementos de la red entre sí, y entre éstos y los nodos de computación. Por su parte, el encaminamiento define los caminos que siguen los paquetes a través de la red. Las prestaciones han sido tradicionalmente la principal métrica a la hora de evaluar las redes de interconexión. Sin embargo, hoy en día hay que considerar dos métricas adicionales: el coste y la tolerancia a fallos. Las redes de interconexión además de escalar en prestaciones también deben hacerlo en coste. Es decir, no sólo tienen que mantener su productividad conforme aumenta el tamaño de la red, sino que tienen que hacerlo sin incrementar sobremanera su coste. Por otra parte, conforme se incrementa el número de nodos en las máquinas de tipo clúster, la red de interconexión debe crecer en concordancia. Este incremento en el número de elementos de la red de interconexión aumenta la probabilidad de aparición de fallos, y por lo tanto, la tolerancia a fallos es prácticamente obligatoria para las redes de interconexión actuales. Esta tesis se centra en la topología fat-tree, ya que es una de las topologías más comúnmente usadas en los clústeres. El objetivo de esta tesis es aprovechar sus características particulares para proporcionar tolerancia a fallos y un algoritmo de encaminamiento capaz de equilibrar la carga de la red proporcionando una buena solución de compromiso entre las prestaciones y el coste. / Gómez Requena, C. (2010). Low-Memory Techniques for Routing and Fault-Tolerance on the Fat-Tree Topology [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/8856 / Palancia

Para beneficiarse de una reducción en la latencia así como disminuir tanto el consumo como el coste, el número óptimo de puertos de un conmutador ha ido aumentando a lo largo del tiempo. Sin embargo, las arquitecturas tradicionales se han quedado atrás bien por bajo rendimiento o bien por problemas de escalabilidad con el número de puertos. En esta Tesis se propone una nueva arquitectura de conmutador válida para conmutadores de elevado grado llamada Partitioned Crossbar Input Queued (PCIQ). Esta arquitectura resuelve el problema de los excesivos requerimientos de memoria en el diseño de arquitecturas de elevado grado. Además PCIQ define una nueva familia de arquitecturas de conmutador. PCIQ se basa en un particionado inteligente del crossbar, dividiéndolo en sub-crossbars, requiriendo menos recursos de memoria que las otras propuestas para conmutadores de elevado grado y que consigue una mayor eficiencia debido en parte a un incremento en la eficiencia de los árbitros empleados en el diseño. En este sentido, PCIQ emplea dos árbitros con prioridad rotativa (uno para cada sub-crossbar) que presentan un coste lineal y una respuesta en el tiempo logarítmica conforme aumenta el número de puertos del conmutador. Además PCIQ tiene un coste (medido en términos de requerimientos de memoria, complejidad del crossbar y complejidad en el arbitraje) similar o incluso menor que organizaciones básicas como CIOQ. No obstante PCIQ es capaz de conseguir máxima eficiencia para distribuciones de tráfico uniforme. El bloqueo por paquete al principio de cola (o HOL en inglés) reduce dramáticamente el rendimiento del conmutador. Las soluciones tradicionales para eliminar el bloqueo por HOL no son escalables con el número de puertos o requieren arquitecturas complejas. En esta Tesis se propone una técnica de control de la congestión que elimina el bloqueo por HOL llamada RECN-IQ. RECN-IQ está diseñada para conmutadores con memorias sólo a la entrada y es una técnica altamente eficiente / Mora Porta, G. (2009). High-performance architectures for high-radix switches [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/4335 / Palancia

This thesis presents a case of study of the development and performance analysis of a surface grading application with real-time compliance. We address the issue of spatial and temporal uniformity in the acquisition system. In a surface grading application it is crucial to ensure the uniform response of the system through time and space. All the results presented for surface grading were obtained using real data from the ceramic tile industry. The VxC TSG database is public and can be accessed at www.disca.upv.es/vision/vxctsg. We present a method based on soft colour-texture descriptors computed in perceptually uniform colour spaces. The method is parameterized and the involved factors are studied using two statistical procedures; experimental design and logistic regression. Although it is not a new theoretical contribution, we have found and demonstrate that a simple set of global colour and texture statistics, together with well-known classifiers, are powerful enough to meet stringent factory requirements for real-time and performance. Also the method is compared with two other approaches from the scientific literature; Colour Histograms and Centile-LBP. Finally, we explore the method's capacity for on-line inspection in a study of real-time compliance and parallelization. / López García, F. (2005). Real-time surface grading of ceramic tiles [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1909 / Palancia

Después de más de 25 años de intensa investigación, la planificación de sistemas de tiempo-real ha mostrado una transición que va desde una infraestructura basada en ejecutivos cíclicos, a modelos de planificación más flexibles, tales como planificación basada en prioridades estáticas y dinámicas, planificación de tareas no críticas, y planificación con retroalimentación, por nombrar algunas. A pesar de lo anterior, actualmente tan sólo unas cuantas políticas de planificación están disponibles para la implementación de sistemas de tiempo-real. Por ejemplo, la mayoría de los sistemas operativos de tiempo-real existentes proporcionan únicamente planificación basada en prioridades fijas. Sin embargo, no todos los requerimientos de las aplicaciones de tiempo-real pueden ser satisfactoriamente atendidos utilizando exclusivamente planificación estática. Existen sistemas constituidos por tareas críticas y no críticas que son planificados de mejor manera utilizando planificación basada en prioridades dinámicas. Además, se ha demostrado que la planificación dinámica permite una mayor utilización de los recursos del sistema. En años recientes, algunos autores han publicado diferentes esquemas para integrar nuevas políticas de planificación a un sistema operativo. Algunos de ellos proponen que los nuevos servicios de planificación se implementen a nivel de usuario, evitando así que la estructura interna del sistema operativo tenga que ser modificada, y ofreciendo la oportunidad de implementar y probar muchos de los resultados generados por el trabajo de investigación en el área de planificación de sistemas de tiempo-real. De entre los trabajos relacionados publicados a la fecha, destaca el Modelo para la Planificación Definida por el Usuario, propuesto por Mario Aldea y Michael González-Harbour. El modelo presenta una Interfaz para Programas de Aplicación (API) que permite crear y utilizar planificadores a nivel de usuario de manera compatible con el modelo de planificación / Díaz Ramírez, A. (2006). Marco de referencia para la definición de planificadores a nivel de usuario en sistemas de tiempo-real [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1934 / Palancia

Actualmente, los clusters de PC son un alternativa rentable a los computadores paralelos. En estos sistemas, miles de componentes (procesadores y/o discos duros) se conectan a través de redes de interconexión de altas prestaciones. Entre las tecnologías de red actualmente disponibles para construir clusters, InfiniBand (IBA) ha emergido como un nuevo estándar de interconexión para clusters. De hecho, ha sido adoptado por muchos de los sistemas más potentes construidos actualmente (lista top500). A medida que el número de nodos aumenta en estos sistemas, la red de interconexión también crece. Junto con el aumento del número de componentes la probabilidad de averías aumenta dramáticamente, y así, la tolerancia a fallos en el sistema en general, y de la red de interconexión en particular, se convierte en una necesidad. Desafortunadamente, la mayor parte de las estrategias de encaminamiento tolerantes a fallos propuestas para los computadores masivamente paralelos no pueden ser aplicadas porque el encaminamiento y las transiciones de canal virtual son deterministas en IBA, lo que impide que los paquetes eviten los fallos. Por lo tanto, son necesarias nuevas estrategias para tolerar fallos. Por ello, esta tesis se centra en proporcionar los niveles adecuados de tolerancia a fallos a los clusters de PC, y en particular a las redes IBA. En esta tesis proponemos y evaluamos varios mecanismos adecuados para las redes de interconexión para clusters. El primer mecanismo para proporcionar tolerancia a fallos en IBA (al que nos referimos como encaminamiento tolerante a fallos basado en transiciones; TFTR) consiste en usar varias rutas disjuntas entre cada par de nodos origen-destino y seleccionar la ruta apropiada en el nodo fuente usando el mecanismo APM proporcionado por IBA. Consiste en migrar las rutas afectadas por el fallo a las rutas alternativas sin fallos. Sin embargo, con este fin, es necesario un algoritmo eficiente de encaminamiento capaz de proporcionar suficientes / Montañana Aliaga, JM. (2008). Efficient mechanisms to provide fault tolerance in interconnection networks for pc clusters [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/2603 / Palancia

Image compression is of great importance in multimedia systems and applications because it drastically reduces bandwidth requirements for transmission and memory requirements for storage. Although earlier standards for image compression were based on the Discrete Cosine Transform (DCT), a recently developed mathematical technique, called Discrete Wavelet Transform (DWT), has been found to be more efficient for image coding. Despite improvements in compression efficiency, wavelet image coders significantly increase memory usage and complexity when compared with DCT-based coders. A major reason for the high memory requirements is that the usual algorithm to compute the wavelet transform requires the entire image to be in memory. Although some proposals reduce the memory usage, they present problems that hinder their implementation. In addition, some wavelet image coders, like SPIHT (which has become a benchmark for wavelet coding), always need to hold the entire image in memory. Regarding the complexity of the coders, SPIHT can be considered quite complex because it performs bit-plane coding with multiple image scans. The wavelet-based JPEG 2000 standard is still more complex because it improves coding efficiency through time-consuming methods, such as an iterative optimization algorithm based on the Lagrange multiplier method, and high-order context modeling. In this thesis, we aim to reduce memory usage and complexity in wavelet-based image coding, while preserving compression efficiency. To this end, a run-length encoder and a tree-based wavelet encoder are proposed. In addition, a new algorithm to efficiently compute the wavelet transform is presented. This algorithm achieves low memory consumption using line-by-line processing, and it employs recursion to automatically place the order in which the wavelet transform is computed, solving some synchronization problems that have not been tackled by previous proposals. The proposed encode / Oliver Gil, JS. (2006). On the design of fast and efficient wavelet image coders with reduced memory usage [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1826 / Palancia

Actualmente, las tecnologías CMOS submicrónicas son básicas para el desarrollo de los modernos sistemas basados en computadores, cuyo uso simplifica enormemente nuestra vida diaria en una gran variedad de entornos, como el gobierno, comercio y banca electrónicos, y el transporte terrestre y aeroespacial. La continua reducción del tamaño de los transistores ha permitido reducir su consumo y aumentar su frecuencia de funcionamiento, obteniendo por ello un mayor rendimiento global. Sin embargo, estas mismas características que mejoran el rendimiento del sistema, afectan negativamente a su confiabilidad. El uso de transistores de tamaño reducido, bajo consumo y alta velocidad, está incrementando la diversidad de fallos que pueden afectar al sistema y su probabilidad de aparición. Por lo tanto, existe un gran interés en desarrollar nuevas y eficientes técnicas para evaluar la confiabilidad, en presencia de fallos, de sistemas fabricados mediante tecnologías submicrónicas. Este problema puede abordarse por medio de la introducción deliberada de fallos en el sistema, técnica conocida como inyección de fallos. En este contexto, la inyección basada en modelos resulta muy interesante, ya que permite evaluar la confiabilidad del sistema en las primeras etapas de su ciclo de desarrollo, reduciendo por tanto el coste asociado a la corrección de errores. Sin embargo, el tiempo de simulación de modelos grandes y complejos imposibilita su aplicación en un gran número de ocasiones. Esta tesis se centra en el uso de dispositivos lógicos programables de tipo FPGA (Field-Programmable Gate Arrays) para acelerar los experimentos de inyección de fallos basados en simulación por medio de su implementación en hardware reconfigurable. Para ello, se extiende la investigación existente en inyección de fallos basada en FPGA en dos direcciones distintas: i) se realiza un estudio de las tecnologías submicrónicas existentes para obtener un conjunto representativo de modelos de fallos transitorios / Andrés Martínez, DD. (2007). Speeding-up model-based fault injection of deep-submicron CMOS fault models through dynamic and partially reconfigurable FPGAS [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1943 / Palancia