Theses Proposals Presentations
These are MAPi students completing the curricular part of the PhD program. They have 20 minutes for their presentation and then follows a discussion period of about 30 minutes.
- Monitoring and Predicting Anomalies in Sensor Network Data Orlando Ohashi (MAPi)
- Relational Databases Digital Preservation, Ricardo Freitas (MAPi)
- Vital Responder Signal Processing and DataAnalysis, Can Ye(MAPi)
- User-Centric Routing, António Júnior(MAPi)
- Distributed Control of Road Traffic based on Vehicular Ad Hoc Networking, Hugo Conceição (MAPi)
- Intelligent Alarm Management System for Large-Scale Telecommunications Companies, Raúl Costa(MAPi)
- Elastic Enterprise Applications, Ana Nunes(MAPi)
- Matrices As Arrows! A Typed Approach to Linear Algebra, Hugo Macedo (MAPi)
- Behavioural certification ofevolvingsoftware requirements, Alexandre Madeira (MAPi)
- Pragmatic Program Transformation and Verification:an Abstract Interpretation Perspective, Vitor Rodrigues(MAPi)
- Secure and Reliable CommunicationInfrastructure for IP-Based Emergency Applications, Vahid Talooki(MAPi)
- Enhancing the Usability, ComputationalEfficiency and Reliability of EEG-based Brain Machine Interfaces, Nuno Figueiredo (MAPi)
- Formal verification of security policies in cryptographic software, Bárbara Vieira(MAPi)
-
Title: Monitoring and Predicting Anomalies in Sensor Network Data
Author: Orlando Ohashi, MAPi 1st Year
Advisors: Luís Torgo (LIAAD/CRACS)
Committee: Advisor, Susana Nascimento (FCT/UNL), Gabriel David (CC-MAPI/UA)
Time: July 6, 9:30
Abstract:
This pre-thesis describes the research area of mining spatio-temporal anomalies in sensor network data, namely monitoring and predicting anomalous values on data streams generated by these sensors. These sensors generate data that are referenced both temporally and geographically. We are interested in developing tools for monitoring and predicting anomalies for this type of networked data. Although generic enough to be applicable to a wide range of application domains in sensor networks, this thesis is guided by a concrete application, monitoring and predicting anomalies in the water distribution network of the metropolitan region of Porto. -
Title: Relational Databases Digital Preservation
Author: Ricardo Freitas, MAPi 1st Year
Advisors: José Carlos Ramalho (CCTC/UM)
Committee: Advisor, Paulo Calado (INESC-ID), Gabriel David (CCTC/UP)
Time: July 7, 12:00
Abstract:
Abstract. Digital preservation is emerging as an area of work and research that tries to provide answers that will ensure a continued and long-term access to information stored digitally. IT Platforms are constantly changing and evolving and nothing can guarantee the continuity of access to digital artifacts in their absence.The preservation of digital objects is extremely complex and far from being stable. Digital objects are software and hardware dependent. Normally, their auto-preservation period is about 5 years. In this context digital preservation practices become very important and should be part of the institutions planning. The problem is how to keep digital objects in such a way that their information is accessible long past their auto-preservation period.
This proposal focus on a specific class of digital objects: Relational Databases; they are the most frequent type of databases used by organizations worldwide. A neutral format that is hardware and software independent is the key to achieve a standard format to use in digital preservation of relational databases. An XML based format, for its neutrality, has high probability to become a standard in this preservation field.
-
Title: Vital Responder Signal Processing and Data Analysis
Author: Can Ye, MAPi 1st Year
Advisors: Miguel Coimbra (IT/FCUP) and Vijayakumar Bhagavatula (ECE/CMU)
Committee: Advisors and José Luís Oliveira (CC-MAPi)
Time: July 6, 14:30
Abstract:
My Ph.D. research focus is on biomedical signal processing and data analysis and is conducted under the framework of the CMU-Portugal research project -- "Vital Responder--Monitoring Stress among First Responder Professionals". The Vital Responder research project aims to explore innovative wearable technologies, provide secure, reliable and effective first-response systems in critical emergency situations and develop biomedical signal processing and pattern recognition solutions for diagnosis and monitoring support, with the emphasis on physiological phenomena, such as fatigue and stress. Specifically, one important goal of Vital Responder is to develop a wearable intelligent garment for monitoring and extracting vital physiological signals, like the electrocardiogram (ECG) and body temperature from the first responders, such as fire fighters, policemen, who are also potential users of Vital Responder technology. My preliminary research has been devoted to exploring relevant public ECG data repositories, analyzing relevant research publications and implementing some relevant algorithms. My preliminary research focus is on the data analysis task, and would provide a solid basis to achieve one of the main objectives of this project, which is the quantification of the effects of stress using signal processing and pattern recognition methodologies (specially in ECG signals). In the near future, we aim to research, develop and implement improved pattern recognition and machine learning algorithms for body stress assessment from ECG signals. Furthermore, we expect that this research may lead to the automatic detection and prediction of critical stress situations, such as heat stroke in fire fighters.
-
Title: User-Centric Routing
Author: António Júnior, MAPi 2nd Year
Advisors: Rute Sofia (INESC-Porto)
Committee: Advisor, Rui Valadas (IST), Paulo Fonseca Pinto (UNL), José Luís Oliveira (CC-MAPi)
Time: July 6, 15:30
Abstract:
The highly nomadic lifestyle of the XXI century is giving rise to new forms of wireless architectures which are user-centric in the sense that the end-user becomes more than a consumer of connectivity. Up until recently, wireless networking assumed that single-source shortest-path routing was the optimal way to approach routing in such dynamic environments. However, wireless architectures attain new requirements which relate to power efficiency, low overhead, low memory, etc. Therefore, protocols devised for multihop routing should incur a very low overhead and be aware of energy problems, in the least. These are some aspects that question the fact that the optimal routing approach to follow is a shortest-path one. Furthermore, considering the user-centric wireless architectures, new requirements arise. These are some of the aspects that the central to the debate on user-centric routing, and which will be discussed in this thesis proposal. -
Title: Distributed Control of Road Traffic based on Vehicular Ad Hoc Networking
Author: Hugo Conceição, MAPi 1st Year
Advisors: Michel Ferreira (IT/FCUP) and Ozan Tonguz (ECE/CMU)
Committee: Advisors, José Luís Oliveira(CC-MAPi)
Time: July 6, 15:30
Abstract:
This document presents the preliminary research done by the author in preparation for his thesis on "Distributed Control of Road Traffic based on Vehicular Ad Hoc Networking".Expansion of roadway capacity has not kept up with the growth in travel, causing significant increases in congestion in major urban areas. Nonrecurring congestion created by crashes or other incidents is a major component of delays experinced by drivers. Acknowledging the problem, the departments of transportation are trying to increase the size of the network they actively monitor to support performance measurement communication. The results are optimisticactivities and real-time management of facilities.
In this work, we evaluate the connectivity in Vehicular Ad-hoc Networks (VANET), a specialization of a Mobile Ad Hoc Network where nodes are vehicles, in order to understand the feasibility of implementing a distributed traffic control based on it. For this study, we make use of computer simulation and propose "Stereoscopic Aerial Photography" as an alternate method to evaluate urban connectivity in VANETs
-
Title: Intelligent Alarm Management System for Large-Scale Telecommunications Companies
Author: Raúl Costa, MAPi 1st Year
Advisors: Paulo Cortez (Algoritmi/UM)
Committee: Advisor,Nuno Cavalheiro Marques (FCT/UNL) , Fernando Silva (CC-MAPi)
Time: July 7, 9:30
Abstract:
This work aims at contribute to the investigation of intelligent alarm management solutions for telecommunication companies. Network elements generate massive amounts of alarm events that must be parsed to detect the source of anomalies. Alarm correlation is performed between identified root-cause alarms and alarms which have been raised on network elements satisfying particular relationships with the network element that raised the root-cause alarm. Current telecommunication networks are heterogeneous and highly dynamic which makes these relations to change continuously.We propose the adoption of data mining algorithms to automatically discover correlation rules from network management centers’ data warehouses. As these rules are not static, machine learning techniques are required to maintain and adapt selected rules in order to upgrade the performance.
-
Title: Elastic Enterprise Applications
Author: Ana Nunes, MAPi 1st Year
Advisors: José Orlando Pereira (CCTC/UM)
Committee: Advisor, Enrique Armendariz (UPNa/Spain), Joaquim Arnaldo Martins (CC-MAPi)
Time: July 7, 11:00
Abstract:
There is a growing awareness of scalability as a key property of enterprise applications.The current target is that IT services are elastic, i.e. that they scale to very large dimensions but also that resources can be provisioned dynamically and incrementally. The motivation for this is twofold: First, to cope with applications with an increasing number of users in a single deployment. Second, to enable the same application to be deployed in increasingly larger settings,allowing a software provider to swiftly capture an emerging market.
We are interested in characterizing the major obstacles for migrating business applications to elastic settings, namely in database-centric applications, in order to propose practical architectural and middleware solutions to overcome them.
This work presents an overview of multi-tier and service-oriented architectures focusing on the abstractions offered in each, with an emphasis on scalability. A database-centric application is presented as a motivational case study, which provides a reference for both reasoning and experimental evaluation.
-
Title: Matrices as Arrows! A Typed Approach to Linear Algebra
Author: Hugo Macedo, MAPi 2nd Year
Advisors: José Nuno Oliveira (CCTC/UM)
Committee: Advisor, Markus Puechel (CMU), Joaquim Arnaldo Martins (CC-MAPi)
Time: July 7, 15:30
Abstract:
This document is a thesis proposal written in the context of the MAPi doctoral programme. It presents the outcome of reviewing the state of the art on domain specific languages devoted to representing matrices and related linear algebra algorithms such as multiplication, transforms and Gaussian limitation for high performance linear algebra library generation. The formalization of such topics using category theory, specially the category of matrices and an index-free calculus developed on top of it is envisaged and a proof of concept is presented. We finish by detailing the objectives, contributions and a time-line we wish to follow to achieve these. -
Title: Behavioural certification of evolving software
requirements
Author: Alexandre Madeira, MAPi 1st Year
Advisors: Luís Barbosa (CCTC/UM) and M. A. Martins (UA)
Committee: Advisor, Razvan Diaconescu (IMAR/Roménia), José Nuno Oliveira (CC-MAPi)
Time: July 8, 9:30
Abstract:
In this pre-thesis, we propose the development of a methodology for behavioral certification of software components with fast evolving requirements, as well as the corresponding theoretical foundations. Our proposal is based on three assumptions: the adoption of property-oriented specifications, the use of classes of dialgebras as models of these specifications, and the consideration of the requirements satisfaction up to behavioral relations. These decisions are concerned with the following factors: property-oriented specifications are easily updated by the introduction of new requirements and are suitable to deal with different specification logics. The dialgebras, as a superset of algebras and coalgebras, seems to be expressive to characterize both algebraic and coalgebraic software aspects on the same structure. The adoption of the behavioral satisfaction is done, not just in order to capture the behavioral semantics of software, but also to entails the structure with appropriate relations to check properties. Beyond the aims, motivations and work plan of the project, an overview of propery-oriented specifications and the exploration of dialgebras as a "mother" of many pertinent structures on the specification process, are presented. For example, the structures of algebras, partial algebras, relational algebras and coalgebras, as well as their categories, are here defined, by adequate instantiations of the defining functors on the category of dialgebras. -
Title: Pragmatic Program Transformation and Verification: an Abstract Interpretation Perspective
Author: Vitor Rodrigues, MAPi 1st Year
Advisors: Simão Sousa (LIACC/UBI) and Mário Florido (LIACC/FCUP)
Committee: Advisors, Isabel Nunes (FCUL), José Nuno Oliveira (CC-MAPi)
Time: July 8, 11:00
Abstract:
Abstract interpretation is explicitly based on a formal semantics definition. A hierarchy of semantics is constructed by successive abstract interpretations and different program semantics definition styles lead to different approaches to program analysis. Examples of applications of the theory of abstract interpretation are dataflow analysis, program transformation and program verification.Extensions to the theory abstract interpretation are based in logical relations, defined inductively on type instead of power domains. Relations have the power to express many aspected of programs such as approximantion of functions, definition of state models, coding of annotated imperative programs, specification of both programs and properties, program transformation and translation algebras, etc.
The purpose of our work is to devise a meta-semantic specification formalism based on binary relations, on top of which we can perform three different operations: a projection algebra that allow us to choose the semantic formalism better adapted to specific taks of verification and transformation of programs; a transformation algebra that allow us to change the level of abstractness of programs by means of abstract/refinement functions; and program verification through the derivation of a verification formalism from the meta-semantic formalism.
The meta-semantic formalism is able to express two different levels of abstraction: the core semantics used by the standard interpretation the abstract semantics used by abstract interpretations. This twofold mechanism allow us to perform verification tasks on specific parts of our programs. In the one hand, we are able to abstract program semantics, using the projection algebra, and apply verification mechanisms on those abstractions. On the other hand, we are able to choose the level of abstractness of our programming language, using the transformation algebra, and apply verification mechanisms on those abstractions. These will be standard tasks in the light of abstract interpretation.
The set of initial objectives we would like to accomplish can be enumerated as follows: (1) build a meta-tool for program analysis, verification and execution, that is independent of the user language and independent of the programming paradigm; (2) integrate operations of program specification, transformation and verification systematically in a unified framework based on abstract interpretation; (3) integrate formal analysis by abstract interpretation in the full software development process, from the initial specifications to the ultimate program development.
-
Title: Secure and Reliable Communication Infrastructure for
IP-Based Emergency Applications
Author: Vahid Talooki, MAPi 1st Year
Advisors: Jonathan Rodriguez (IT/UA)
Committee: Advisor, Paulo Machado (IT/UPCB), José Valença (CC-MAPi)
Time: July 8, 14:30
Abstract:
This PhD work investigates a secure and reliable communication infrastructure for IP-Based emergency applications. Handling communication in extreme emergency cases like flooding, earthquake, accident, terrorist attacks, disaster and so on needs some robustness and reliable networks which can be setting up easily and don't need to heavy infrastructure.Mobile Ad hoc Networks (MANET) is an ideal tool for this reason. Ad hoc networks are characterized by multi-hop wireless connectivity and frequently changing network topology which have made them infrastructure less. Each mobile node operates not only as a host but also as a router and forwards packets for other mobile nodes in the network that may not be within direct transmission range of each other. So this network doesn't need to infrastructure and can be installed quickly.
This work Investigate and realize mechanisms for providing reliable services in IP networks in general and ad-hoc networks in particular. To achieve this goal we will consider to reliable routing schemes in MANET which can be useful for extreme emergency cases. Beside that providing mechanisms for identifying DOS attacks and triggering appropriate defence solutions will be considered.
-
Title: Enhancing the Usability, Computational Efficiency and Reliability of EEG-based Brain Machine Interfaces
Author: Nuno Figueiredo, MAPi 1st Year
Advisors: Filipe Silva (IEETA/UA) and Petia Giorgieva (IEETA/UA)
Committee: Advisors, José Carlos Principe (UFL/US), Fernando Silva (CC-MAPi)
Time: July 8, 15:30
Abstract:
A Brain Machine Interface (BMI) is a communication channel between the human brain and the surrounding world. A common method for designing a noninvasive BMI is to use electroencephalogram (EEG) signals during mental tasks, sensory motor tasks or visual stimulation. The conceptual approach is to identify electric brain activity variations and map them into some kind of actuation or command over a target output (e.g., a computer interface or a robotic device). Over the last decade the BMIs gain a growing interest in the fields of multimedia and human-computer interaction, however their main objective is to improve the life quality of paralyzed people or those suffering from severe neuromuscular disorders. Continuing advances have supported the idea that the BMI concept is viable, although a significant research and development effort has to be conducted to improve the functionality, efficiency and usability of the actual BMIs. For example, reliable techniques for advanced signal processing and pattern recognition that are able to extract meaningful information from the very noisy EEG signals are still a challenging issue.The planed PhD work is going to address one of the main challenges in the BMI area: the usability. In order to improve the usability, the problem of minimum number of BMI electrodes will be one of the main topics of this study. The minimization of the number of electrodes reduces the quantity of data to be processed and the processing resources needed to operate a BMI device. It is expected that this will turn the BMI system more user friendly, more robust and practical to implement and hopefully less noisy and time demand which is crucial for on-line applications.
A key issue related with the minimization of the electrodes number is the localization of the electrodes on the scalp. In this sense, it is planed to extend the typical EEG-based non-invasive BMI strategy with simultaneous analysis of EEG and functional Magneto Resonance Images (fMRIs). The strategy envisaged is to study in a systematic way the correlation of electrical brain activity (EEG) and the blood oxygen level dependent (BOLD) response, measured by the fMRI with human's mental states in order to improve the quality of the EEG signals and gain deeper insight about the effects of training, long term use and feedback. It is expected that the minimization and the correct electrode localization is a subject dependent issue and therefore the ambitions of the forthcoming research is to build a personalized BMI system that reflects the individual human brain most active zones.
-
Title: Formal verification of security policies in cryptographic software
Author: Bárbara Vieira, MAPi 1st Year
Advisors: Manuel Barbosa (CCTC/UM)
Committee: Advisor, Simão Sousa (UBI), José Valença (CC-MAPi)
Time: July 8, 17:00
Abstract:
Security is notoriously difficult to sell as a feature in software products. In addition to meeting a set of security requirements, cryptographic software has to be cheap, fast, and use little resources. The development of cryptographic software is an area with specific needs in terms of software development processes and tools. The CACE European project aims to develop a tool-box that assists programmers in producing high-quality cryptographic code.This work stems from Work-package 5 in the CACE project, which targets the incorporation in the CACE tool-box of language-based techniques capable of providing assurance that cryptographic software implementations enforce desired security policies. This thesis proposal is organized in four parts.
The first part focuses on the different security policies that may be at play in software systems, and the identification of relevant security requirements in the context of cryptographic software.
The second part contains an overview of language-based security techniques, together with an evaluation of those techniques that are best suited to formalise and verify the security policies identified in part one.
In the third part we present an in-depth study of a deductive verification tool integrated in Frama-c framework, as well as the application of new methodologies based on deductive verification to formalise and verify relevant security policies in cryptographic software. We also present a case-study of the Frama-c tool.
The last part is related with the design of a deductive verification tool for a cryptographic programming language (CAO) that is being developed in the CACE project.