Předmětem dizertační práce je návrh nových technik pro verifikaci hardwaru, které jsou optimalizovány pro použití v procesu souběžného vývoje hardwaru a softwaru. V rámci tohoto typu vývoje je hardware spolu se software vyvíjen paralelně s cílem urychlit vývoj nových systémů. Současné nástroje pro tvorbu mikroprocesorů stavějící na tomto stylu vývoje obvykle umožňují vývojářům ověřit jejich návrh využitím různých simulačních technik a/nebo za pomoci tzv. funkční verifikace. Společnou nevýhodou těchto přístupů je, že se zaměřují pouze na hledání chyb. Výsledný produkt tedy může stále obsahovat nenalezené netriviální defekty. Z tohoto důvodu se v posledních letech stává stále více žádané nasazení formálních metod. Na rozdíl od výše uvedených přístupů založených na hledání chyb, se formální verifikace zaměřuje na dodání rigorózního důkazu, že daný systém skutečně splňuje požadované vlastnosti. I když bylo v uplynulých letech v této oblasti dosaženo značného pokroku, tak aktuální formální přístupy nemají zdaleka schopnost plně automaticky prověřit všechny relevantní vlastnosti verifikovaného návrhu bez výrazného a často nákladného zapojení lidí v rámci verifikačního procesu. Tato práce se snaží řešit problém s automatizací verifikačního procesu jejím zaměřením na verifikační techniky, ve kterých je záměrně kladen menší důraz na jejich přesnost a obecnost, za cenu dosažení plné automatizace (např. vyloučením potřeby ručně vytvářet modely prostředí). Dále se práce také zaměřuje na efektivitu navrhovaných technik a jejich schopnost poskytovat nepřetržitou zpětnou vazbu o verifikačním procesu (např. v podobě podání informace o aktuálním stavu pokrytí). Zvláštní pozornost je pak věnována vývoji formálních metod ověřujících ekvivalenci návrhů mikroprocesorů na různých úrovních abstrakce. Tyto návrhy se mohou lišit ve způsobu, jakým jsou vnitřně zpracovány programové instrukce, nicméně z vnějšího pohledu (daného např. obsahem registrů viditelných z pozice programátora) musí být jejich chování při provádění stejného vstupního programu shodné. Kromě těchto témat se práce také zabývá problematikou návrhu metod pro verifikaci správnosti mechanismů zabraňujících výskytu datových a řídících hazardů v rámci linky zřetězeného zpracování instrukcí. Veškeré metody popsané v této práci byly implementovány ve formě několika nástrojů. Aplikací těchto nástrojů pro verifikaci návrhů netriviálních procesorů bylo dosaženo slibných experimentálních výsledků.

Cloud computing represents a fundamental change in the way organizations acquire technological resources (e.g., hardware, development and execution environments, applications); where, instead of buying them, they acquire remote access to them in the form of cloud services supplied through the Internet. Among the main characteristics of cloud computing is the allocation of resources in an agile and elastic way, reserved or released depending on the demand of the users or applications, enabling the payment model based on consumption metrics. The development of cloud applications mostly follows an incremental approach, where the incremental delivery of functionalities to the client changes - or reconfigures - successively the current architecture of the application. Cloud providers have their own standards for both implementation technologies and service management mechanisms, requiring solutions that facilitate: building, integrating and deploying portable services; interoperability between services deployed across different cloud providers; and continuity In the execution of the application while its architecture is reconfigured product of the integration of the successive increments. The principles of the model-driven development approach, the architectural style service-oriented architectures, and the dynamic reconfiguration play an important role in this context. The hypothesis of this doctoral thesis is that model-driven development methods provide cloud service developers with abstraction and automation mechanisms for the systematic application of the principles of model engineering during the design, implementation, and incremental deployment of cloud services, facilitating the dynamic reconfiguration of the service-oriented architecture of cloud applications. The main objective of this doctoral thesis is therefore to define and validate empirically DIARy, a method of dynamic and incremental reconfiguration of service-oriented architectures for cloud applications. This method will allow specifying the architectural integration of the increment with the current cloud application, and with this information to automate the derivation of implementation artifacts that facilitate the integration and dynamic reconfiguration of the service architecture of the cloud application. This dynamic reconfiguration is achieved by running reconfiguration artifacts that not only deploy / un-deploy increment's services and orchestration services between services of the increment with the services of the current cloud application; but also, they change the links between services at runtime. A software infrastructure that supports the activities of the proposed method has also been designed and implemented. The software infrastructure includes the following components: i) a set of DSLs, with their respective graphical editors, that allow to describe aspects related to the architectural integration, implementation and provisioning of increments in cloud environments; ii) transformations that generate platform-specific implementation and provisioning models; (iii) transformations that generate artifacts that implement integration logic and orchestration of services, and scripts of provisioning, deployment, and dynamic reconfiguration for different cloud vendors. This doctoral thesis contributes to the field of service-oriented architectures and in particular to the dynamic reconfiguration of cloud services architectures in an iterative and incremental development context. The main contribution is a well-defined method, based on the principles of model-driven development, which makes it easy to raise the level of abstraction and automate, through transformations, the generation of artifacts that perform the dynamic reconfiguration of cloud applications. / La computación cloud representa un cambio fundamental en la manera en la que las organizaciones adquieren recursos tecnológicos (p. ej., hardware, entornos de desarrollo y ejecución, aplicaciones); en donde, en lugar de comprarlos adquieren acceso remoto a ellos en forma de servicios cloud suministrados a través de Internet. Entre las principales características de la computación cloud está la asignación de recursos de manera ágil y elástica, reservados o liberados dependiendo de la demanda de los usuarios o aplicaciones, posibilitando el modelo de pago basado en métricas de consumo. El desarrollo de aplicaciones cloud sigue mayoritariamente un enfoque incremental, en donde la entrega incremental de funcionalidades al cliente cambia - o reconfigura - sucesivamente la arquitectura actual de la aplicación. Los proveedores cloud tienen sus propios estándares tanto para las tecnologías de implementación como para los mecanismos de gestión de servicios, requiriéndose soluciones que faciliten: la construcción, integración y despliegue de servicios portables; la interoperabilidad entre servicios desplegados en diferentes proveedores cloud; y la continuidad en la ejecución de la aplicación mientras su arquitectura es reconfigurada producto de la integración de los sucesivos incrementos. Los principios del enfoque de desarrollo dirigido por modelos, del estilo arquitectónico de arquitecturas orientadas a servicios y de la reconfiguración dinámica cumplen un papel importante en este contexto. La hipótesis de esta tesis doctoral es que los métodos de desarrollo dirigido por modelos brindan a los desarrolladores de servicios cloud mecanismos de abstracción y automatización para la aplicación sistemática de los principios de la ingeniería de modelos durante el diseño, implementación y despliegue incremental de servicios cloud, facilitando la reconfiguración dinámica de la arquitectura orientada a servicios de las aplicaciones cloud. El objetivo principal de esta tesis doctoral es por tanto definir y validar empíricamente DIARy, un método de reconfiguración dinámica e incremental de arquitecturas orientadas a servicios. Este método permitirá especificar la integración arquitectónica del incremento con la aplicación cloud actual, y con esta información automatizar la derivación de los artefactos de implementación que faciliten la integración y reconfiguración dinámica de la arquitectura de servicios de la aplicación cloud. Esta reconfiguración dinámica se consigue al ejecutar los artefactos de reconfiguración que no solo despliegan/repliegan los servicios del incremento y servicios de orquestación entre los servicios del incremento con los servicios de la aplicación cloud actual; sino también, cambian en tiempo de ejecución los enlaces entre servicios. También se ha diseñado e implementado una infraestructura software que soporta las actividades del método propuesto e incluye los siguientes componentes: i) un conjunto de DSLs, con sus respectivos editores gráficos, que permiten describir aspectos relacionados a la integración arquitectónica, implementación y aprovisionamiento de incrementos en entornos cloud; ii) transformaciones que generan modelos de implementación y aprovisionamiento; iii) transformaciones que generan artefactos que implementan la lógica de integración y orquestación de servicios, y scripts de aprovisionamiento, despliegue y reconfiguración dinámica específicos para distintos proveedores cloud. Esta tesis doctoral contribuye al campo de las arquitecturas orientadas a servicios y en particular a la reconfiguración dinámica de arquitecturas de servicios cloud en contextos de desarrollo iterativo e incremental. El principal aporte es un método bien definido, basado en los principios del desarrollo dirigido por modelos, que facilita elevar el nivel de abstracción y automatizar por medio de transformaciones la generación de artefactos que real / La computació cloud representa un canvi fonamental en la manera en què les organitzacions adquirixen recursos tecnològics (ej., maquinari, entorns de desplegament i execució, aplicacions) ; on, en compte de comprar-los adquirixen accés remot a ells en forma de servicis cloud subministrats a través d'Internet. Entre les principals característiques de la computació cloud els recursos cloud són assignats de manera àgil i elàstica, reservats o alliberats depenent de la demanda dels usuaris o aplicacions, possibilitant el model de pagament basat en mètriques de consum. El desenrotllament d'aplicacions cloud seguix majoritàriament un enfocament incremental, on l'entrega incremental de funcionalitats al client canvia - o reconfigura - successivament l'arquitectura actual de l'aplicació. Els proveïdors cloud tenen els seus propis estàndards tant per a les tecnologies d'implementació com per als mecanismes de gestió de servicis, requerint-se solucions que faciliten: la construcció, integració i desplegament de servicis portables; la interoperabilitat entre servicis desplegats en diferents proveïdors cloud; i la continuïtat en l'execució de l'aplicació mentres la seua arquitectura és reconfigurada producte de la integració dels successius increments. Els principis de l'enfocament de desenrotllament dirigit per models, de l'estil arquitectònic d'arquitectures orientades a servicis i de la reconfiguració dinàmica complixen un paper important en este context. La hipòtesi d'esta tesi doctoral és que els mètodes de desenrotllament dirigit per models brinden als desenvolupadors de servicis cloud mecanismes d'abstracció i automatització per a l'aplicació sistemàtica dels principis de l'enginyeria de models durant el disseny, implementació i desplegament incremental de servicis cloud, facilitant la reconfiguració dinàmica de l'arquitectura orientada a servicis de les aplicacions cloud. L'objectiu principal d'esta tesi doctoral és per tant de definir i validar empí-ricamente DIARy, un mètode de reconfiguració dinàmica i incremental d'arquitectures orientades a servicis per a aplicacions cloud. Este mètode permetrà especificar la integració arquitectònica de l'increment amb l'aplicació cloud actual, i amb esta informació automatitzar la derivació dels artefactes d'implementació que faciliten la integració i reconfiguració dinàmica de l'arquitectura de servicis de l'aplicació cloud. Esta reconfi-guración dinàmica s'aconseguix a l'executar els artefactes de reconfiguració que no sols despleguen/repleguen els servicis de l'increment i servicis d'orquestració entre els servicis de l'increment amb els servicis de l'aplicació cloud actual; sinó també, canvien en temps d'execució els enllaços entre servicis. També s'ha dissenyat i implementat una infraestructura programari que suporta les activitats del mètode proposat i inclou els següents components: i) un conjunt de DSLs, amb els seus respectius editors gràfics, que permeten descriure aspectes relacionats a la integració arquitectònica, implementació i aprovisionament en entorns cloud dels increments; ii) transformacions que generen models d'implementació i aprovisionament específics de la plataforma a partir dels models d'integració d'alt nivell; iii) transformacions que generen artefactes que implementen la lògica d'integració i orquestració de servicis, i scripts d'aprovisionament, desplegament i reconfiguració dinàmica específics per a distints proveïdors cloud. Esta tesi doctoral contribuïx al camp de les arquitectures orientades a servicis i en particular a la reconfiguració dinàmica d'arquitectures de servicis cloud en contextos de desenrotllament iteratiu i incremental. La principal aportació és un mètode ben definit, basat en els principis del desenrotllament dirigit per models, que facilita elevar el nivell d'abstracció i automatitzar per mitjà de transformacions la generació d'artefactes que r / Zuñiga Prieto, MÁ. (2017). Reconfiguración Dinámica e Incremental de Arquitecturas de Servicios Cloud Dirigida por Modelos [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/86288

From the 1970s to the present time, the World Health Organization (WHO) explains the importance of health promotion in the world. The increased interest in promoting health and increasing health costs for the economies contributed to the recognition of health care as an important area of research. One of the most important aspects of these research currently is the Telehealth, using Information and Communication Technologies (ICT) to try to provide universal access to health. The use of Interactive Digital TV technology helps in accessing remote locations and creates the opportunity to distribute applications across their infrastructure. Dealing with the problems that arise from the convergence of these concepts is of great importance. The architectural description process helps in the development of applications and systems based on the referenced concepts. However, there are no frameworks to help the description of architectures for this particular domain. This paper proposes the ARCHealth an enterprise architecture framework created to assist the architecture development process in accordance with ISO/IEC/IEEE 42010:2011. The ARCHealth was based on the principles of primary health care, taking into account the main concerns of stakeholders and the specific area. / Desde a década de 1970 até o presente momento, a Organização Mundial da Saúde (OMS) expõe a importância da promoção da saúde no mundo. O aumento do interesse na promoção da saúde e os custos de saúde crescentes para as economias contribuíram para o reconhecimento dos cuidados à saúde como uma importante área de pesquisa. Uma das vertentes mais importantes dessas pesquisas atualmente, é a Telehealth, que utiliza das Tecnologias de Informação e Comunicação (TIC) para tentar prover acesso universal à saúde. O uso da TV Digital Interativa auxilia no acesso a locais remotos e cria a oportunidade de distribuir aplicações através de sua infraestrutura. Lidar com os problemas que surgem a partir da convergência desses conceitos é de grande importância. O processo de descrição de arquitetura auxilia no desenvolvimento de aplicações e sistemas baseados nos conceitos referenciados. Porém, não existem muitos frameworks que auxiliem a descrição de arquiteturas para esse domínio específico. Este trabalho propõe o ARCHealth, um enterprise architecture framework criado para auxiliar o processo de desenvolvimento de arquitetura em conformidade com a norma ISO/IEC/IEEE 42010:2011. O ARCHealth foi elaborado com base nos princípios de Atenção Primária à Saúde, levando em consideração as principais preocupações das partes interessadas e do domínio específico.

Analýza softwaru je metodologie, jejímž účelem je analyzovat chování daného programu. Jednotlivé metody této analýzy je možné využít i v dalších oborech, jako je zpětné inženýrství, migrace kódu apod. V této práci se zaměříme na analýzu strojového kódu, na zjištění nedostatků existujících metod a na návrh metod nových, které umožní rychlou a přesnou rekonfigurovatelnou analýzu kódu (tj. budou nezávislé na konkrétní cílové platformě). Zkoumány budou dva typy analýz - dynamická (tj. analýza za běhu aplikace) a statická (tj. analýza aplikace bez jejího spuštění). Přínos této práce v rámci dynamické analýzy je realizován jako rekonfigurovatelný ladicí nástroj a dále jako dva typy tzv. rekonfigurovatelného translátovaného simulátoru. Přínos v rámci statické analýzy spočívá v navržení a implementování rekonfigurovatelného zpětného překladače, který slouží pro transformaci strojového kódu zpět do vysokoúrovňové reprezentace. Všechny tyto nástroje jsou založeny na nových metodách navržených autorem této práce. Na základě experimentálních výsledků a ohlasů od uživatelů je možné usuzovat, že tyto nástroje jsou plně srovnatelné s existujícími (komerčními) nástroji a nezřídka dosahují i lepších výsledků.