Recent Publications

Curzon P, Masci P, Oladimeji P, Ruksenas R, Thimbleby H, D'Urso E.  2014.  Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project. 2nd Workshop on Verification and Assurance (Verisure2014), in association with Computer-Aided Verification (CAV), part of the Vienna Summer of Logic. Abstractverisure14.pdf

The number of recalls of medical device with embedded computers due to safety issues in recent years suggests there is a need for new approaches to support the process. There is increasing concern about the impact of systematic use errors. There has been little research focusing on model-based tool support for the assurance and certification of medical devices with respect to systematic use error, however. The CHI+MED project (http://www.chi-med.ac.uk) aims to address this gap. It is concerned with the design of safer medical devices with a specific focus on human-computer interaction. We are developing a range of integrated model-based engineering methods and other formal and semi-formal techniques to support the certification process, both pre- and post-market, including their use in the wider system context. In this position paper we review our approach and the contributions to date.

Bernardeschi C, Domenici A, Masci P.  2014.  Integrated Simulation of Implantable Cardiac Pacemaker Software and Heart Models. Proceedings of the 2nd International Congress on Cardiovascular Technologies. 2014_cardiotechnix.pdf
Pacheco H, Zan T, Hu Z.  2014.  BiFluX: A Bidirectional Functional Update Language for XML. Accepted to the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014). Abstract
n/a
Hu Z, Pacheco H, Fischer S.  2014.  Validity Checking of Putback Transformations in Bidirectional Programming (Invited paper). Proceedings of the 19th International Symposium on Formal Methods (FM 2014). :1–15. Abstract
n/a
Zan T, Pacheco H, Hu Z.  2014.  Writing Bidirectional Model Transformations as Intentional Updates (Nier track). Companion Proceedings of the 36th International Conference on Software Engineering (ICSE Companion 2014). :488–491. Abstract
n/a
Pacheco H, Hu Z, Fischer S.  2014.  Monadic Combinators for ``Putback'' Style Bidirectional Programming. Proceedings of the 22th ACM SIGPLAN Workshop on Partial evaluation and Program Manipulation (PEPM 2014). :39–50. Abstract
n/a
Silva JMC, Carvalho P, Lima SR.  2014.  A Modular Architecture for Deploying Self-adaptive Traffic Sampling. Monitoring and Securing Virtualized Networks and Services: 8th IFIP WG 6.6 International Conference on Autonomous Infrastructure, Management, and Security, AIMS 2014, Brno, Czech Republic, June 30 – July 3, 2014. Proceedings. :179–183. Abstract

n/a

Silva JMC, Carvalho P, Lima SR.  2014.  Computational weight of network traffic sampling techniques. 2014 IEEE Symposium on Computers and Communications (ISCC). :1-6. Abstract
n/a
Lima R, Moreno CB, Miranda H.  2013.  Broadcast Cancellation in Search Mechanisms. Proceedings of the 28th Annual ACM Symposium on Applied Computing - SAC. Abstractsac2013_2.pdf

Searching for resources over unstructured networks is usually supported by broadcast communication primitives. Ideally, the broadcast process should be cancelled as soon as possible after a successful discovery, to avoid ooding the entire network. However, cancelling an ongoing broadcast is challenging and may increase the number of exchanged messages.
In this paper, we compare the cancellation mechanisms used by BERS and BERS? With new proposed cancellation approaches BCIR and BCIR? The formulation of a simpli ed analytical model and the simulation results show that:i)it is possible to reduce the number of retransmitted messages, without increasing the latency observed in BERS?; and ii) BCIR is more energy ecient, which can contribute to extend the availability of mobile battery powered devices.

Terelius H, Varagnolo D, Moreno CB, Johansson KH.  2013.  Fast distributed estimation of empirical mass functions over anonymous networks. IEEE 52nd Annual Conference on Decision and Control (CDC). Abstractcdc2013.pdf

The aggregation and estimation of values over networks is fundamental for distributed applications, such as wireless sensor networks. Estimating the average, minimal and maximal values has already been extensively studied in the literature. In this paper, we focus on estimating empirical distributions of values in a network with anonymous agents. In particular, we compare two different estimation strategies in terms of their convergence speed, accuracy and communication costs. The first strategy is deterministic and based on the average consensus protocol, while the second strategy is probabilistic and based on the max consensus protocol.

Oliveira JP, Pereira JO.  2013.  Experience with a Middleware Infrastructure for Service Oriented Financial Applications. 28th ACM Symposium on Applied computing (SAC) - Dependable and Adaptive Distributed Systems. Abstractop13.pdf

Financial institutions, acting as financial intermediaries, need to handle numerous information sources and feed them to multiple processing, storage, and display services. This requires filtering and routing, but these feeds are usually provided in custom formats and protocols that are not the best fit for further processing. Moreover, the sheer volume of information and stringent timeliness and reliability requirements make this a substantial task.
In this paper,
i)
we characterize one of these information feeds (the Exchange Data Publisher feed from the NYSE Euronext European Cash Markets) and
ii)
we present and evaluate a dissemination system for this particular feeder based on commodity hardware and open-source message-oriented middleware (Apache Qpid). This allows us to assess the feasibility of this approach and to point out the main challenges to be overcome.

Cruz F, Maia F, Matos M, Oliveira R, Paulo J, Pereira JO, Vilaça R.  2013.  MeT: Workload aware elasticity for NoSQL. Proceedings of the 8th European Conference on Computer Systems - EuroSys. :183–196. Abstractmet.pdf

NoSQL databases manage the bulk of data produced by modern Web applications such as social networks. This stems from their ability to partition and spread data to all available nodes, allowing NoSQL systems to scale. Unfortunately, current solutions' scale out is oblivious to the underlying data access patterns, resulting in both highly skewed load across nodes and suboptimal node configurations.
In this paper, we first show that judicious placement of HBase partitions taking into account data access patterns can improve overall throughput by 35%. Next, we go beyond current state of the art elastic systems limited to uninformed replica addition and removal by: i) reconfiguring existing replicas according to access patterns and ii) adding replicas specifically configured to the expected access pattern.
MeT is a prototype for a Cloud-enabled framework that can be used alone or in conjunction with OpenStack for the automatic and heterogeneous reconfiguration of a HBase deployment. Our evaluation, conducted using the YCSB workload generator and a TPC-C workload, shows that MeT is able to i) autonomously achieve the performance of a manual configured cluster and ii) quickly reconfigure the cluster according to unpredicted workload changes.

Barbosa MB, Farshim P.  2013.  On the Semantic Security of Functional Encryption Schemes. The 16th International Conference on Practice and Theory in Public Key Cryptography - PKC. :143-161. Abstract474.pdf

Functional encryption (FE) is a powerful cryptographic primitive that generalizes many asymmetric encryption systems proposed in recent years. Syntax and security definitions for FE were proposed by Boneh, Sahai, and Waters (BSW) (TCC 2011) and independently by O’Neill (ePrint 2010/556). In this paper we revisit these definitions, identify several shortcomings in them, and propose a new definitional approach that overcomes these limitations. Our definitions display good compositionality properties and allow us to obtain new feasibility and impossibility results for adaptive token-extraction attack scenarios that shed further light on the potential reach of general FE for practical applications.

Paulo J, Pereira JO.  2013.  DEDIS: Distributed Exact Deduplication for Primary Storage Infrastructures. Poster abstract In proceedings of Symposium on Cloud Computing . Abstractpp13.pdf

Deduplication is now widely accepted as an efficient technique for reducing storage costs at the expense of some processing overhead, being increasingly sought in primary storage systems and cloud computing infrastructures holding Virtual Machine (VM) volumes. Besides a large number of duplicates that can be found across static VM images, dynamic general purpose data from VM volumes allows space savings from 58% up to 80% if deduplicated in a cluster-wide fashion. However, some of these volumes persist latency sensitive data which limits the overhead that can be incurred in I/O operations. Therefore, this problem must be addressed by a cluster-wide distributed deduplication system for such primary storage volumes.

Coelho F, Cruz F, Pereira JO, Vilaça R, Oliveira R.  2013.  pH1: middleware transaccional para NoSQL. INFORUM - Simpósio de Informática. Abstractph1.pdf

As bases de dados NoSQL optam por não oferecer importantes abstracções tradicionalmente encontradas nas bases de dados relacionais, de modo a atingir elevada escalabilidade e disponibilidade: garantias transacionais e critérios de coerência de dados fortes. Estas limitações resultam em maior complexidade no desenvolvimento de aplicações sobre bases de dados NoSQL e, logo, são um obstáculo à adoção do paradigma. Neste trabalho, propomos uma camada de middleware sobre bases de dados NoSQL que oferece garantias transacionais com Snapshot Isolation. A abordagem é não-intrusiva, apresentando aos clientes a mesma interface NoSQL acrescida do contexto transacional. Este contexto transacional é o cerne da nossa contribuição e assenta modularmente num repositório distribuído, não persistente, que mantém várias versões dos dados manipulados e num certificador de transaçõess concorrentes. Apresentamos uma implementação do nosso sistema pH1 sobre Cassandra e, recorrendo a um benchmark (YCSB) extensamente utilizado na avaliação de desempenho de bases de dados NoSQL, medimos o custo do suporte do paradigma transacional com garantias transacionais ACID, que não resulta numa diminuição significativa da latência das operações quando comparado com o Cassandra.