Desenvolvimento de um BMS para aplicações de mobilidade elétrica

Dissertação de mestrado integrado em Engenharia Eletrónica Industrial e de Computadores

Gestão e instalação de redes de sensores sem fios (domótica)

Dissertação de mestrado integrado em Engenharia Eletrónica Industrial e Computadores

Personalized-based dietary recommendation for weightlifting

Dissertação de mestrado integrado em Engenharia Eletrónica Industrial e Computadores

Desenvolvimento de um processador VLIW

Dissertação de mestrado integrado em Engenharia Eletrónica Industrial e Computadores

Seguidor do ponto de máxima potência multi-conversor para sistemas solares fotovoltaicos

Dissertação de mestrado integrado em Engenharia Eletrónica Industrial e de Computadores

Desenvolvimento e otimização do projeto mecatrónico de um tribómetro rotativo (FRICTORQ)

Dissertação de mestrado integrado em Engenharia Mecânica

Quantifying, generating and mitigating radio interference in Low-Power Wireless Networks

Doctoral Programme in Telecommunication - MAP-tele

All over the place localization system

The MAP-i Doctoral Programme in Informatics, of the Universities of Minho, Aveiro and Porto

Multithreading RTOS processor design

Tese de Doutoramento Plano Doutoral em Engenharia Eletrónica e de Computadores.

Hybrid hypervisor partially deployed on FPGA

Tese de Doutoramento em Engenharia Eletrónica e Computadores.

Utilização de computação de elevado desempenho para a simulação de problemas de hidrodinâmica costeira

Dissertação de mestrado integrado em Engenharia Civil

A study of risk-aware program transformation

In the trend towards tolerating hardware unreliability, accuracy is exchanged for cost savings. Running on less reliable machines, functionally correct code becomes risky and one needs to know how risk propagates so as to mitigate it. Risk estimation, however, seems to live outside the average programmer’s technical competence and core practice. In this paper we propose that program design by source-to-source transformation be risk-aware in the sense of making probabilistic faults visible and supporting equational reasoning on the probabilistic behaviour of programs caused by faults. This reasoning is carried out in a linear algebra extension to the standard, `a la Bird-Moor algebra of programming. This paper studies, in particular, the propagation of faults across standard program transformation techniques known as tupling and fusion, enabling the fault of the whole to be expressed in terms of the faults of its parts.

Refinement in hybridised institutions

Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of reconfigurable systems, i.e., systems with reconfiguration mechanisms governing the dynamic evolution of their execution configurations in response to both external stimuli or internal performance measures. A formal representation of such systems is through transition structures whose states correspond to the different configurations they may adopt. Therefore, each node is endowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. This paper characterises equivalence and refinement for these sorts of models in a way which is independent of (or parametric on) whatever logic (propositional, equational, fuzzy, etc) is found appropriate to describe the local configurations. A Hennessy–Milner like theorem is proved for hybridised logics.

On the verification of architectural reconfigurations

In a reconfigurable system, the response to contextual or internal change may trigger reconfiguration events which, on their turn, activate scripts that change the system׳s architecture at runtime. To be safe, however, such reconfigurations are expected to obey the fundamental principles originally specified by its architect. This paper introduces an approach to ensure that such principles are observed along reconfigurations by verifying them against concrete specifications in a suitable logic. Architectures, reconfiguration scripts, and principles are specified in Archery, an architectural description language with formal semantics. Principles are encoded as constraints, which become formulas of a two-layer graded hybrid logic, where the upper layer restricts reconfigurations, and the lower layer constrains the resulting configurations. Constraints are verified by translating them into logic formulas, which are interpreted over models derived from Archery specifications of architectures and reconfigurations. Suitable notions of bisimulation and refinement, to which the architect may resort to compare configurations, are given, and their relationship with modal validity is discussed.

Análise técnica - económica da produção de energia em sistemas de abastecimento de água: caso do aproveitamento de fins múltiplos dos socorridos

Dissertação de mestrado integrado em Engenharia Civil