Abstract
The Message Passing Interface (MPI) is the de facto standard message-passing infrastructure for developing parallel applications. Two decades after the first version of the library specification, MPI-based applications are nowadays routinely deployed on super and cluster computers. These applications, written in C or Fortran, exhibit intricate message passing behaviours, making it hard to statically verify important properties such as the absence of deadlocks. Our work builds on session types, a theory for describing protocols that provides for correct-by-construction guarantees in this regard. We annotate MPI primitives and C code with session type contracts, written in the language of a software verifier for C. Annotated code is then checked for correctness with the software verifier. We present preliminary results and discuss the challenges that lie ahead for verifying realistic MPI program compliance against session types.

Abstract

Abstract
Critical monitoring applications can use wireless sensor networks to transport delay sensitive data. This data may demand bounded delays in order to be considered useful by the receiver. In these cases, an accurate and real-time estimation of the end-to-end delay could be used to anticipate the data usefulness prior to sending it. A novel real-time and end-to-end delay estimation mechanism is proposed in this paper, which considers processing times and two new RPL metrics. Results show that our proposal is more accurate than the ETT-based solution for delay estimation, and it does not significantly degrade the network performance.

Abstract
Scientific publications are the main vehicle to disseminate information in the field of biotechnology for wastewater treatment. Indeed, the new research paradigms and the application of high-throughput technologies have increased the rate of publication considerably. The problem is that manual curation becomes harder, prone-to-errors and time-consuming, leading to a probable loss of information and inefficient knowledge acquisition. As a result, research outputs are hardly reaching engineers, hampering the calibration of mathematical models used to optimize the stability and performance of biotechnological systems. In this context, we have developed a data curation workflow, based on text mining techniques, to extract numerical parameters from scientific literature, and applied it to the biotechnology domain. A workflow was built to process wastewater-related articles with the main goal of identifying physico-chemical parameters mentioned in the text. This work describes the implementation of the workflow, identifies achievements and current limitations in the overall process, and presents the results obtained for a corpus of 50 full-text documents.

Abstract
Monitoring and managing traffic are vital elements to the operation of a network. Traffic prediction is an essential tool that captures the underlying behavior of a network and can be used, for example, to detect anomalies by defining acceptable data traffic thresholds. In this context, most current solutions are heavily based on historical time data, which makes it difficult to employ them in a dynamic environment such as cloud computing. We propose a traffic prediction approach based on a statistical model where observations are weighted with a Poisson distribution inside a sliding window. The evaluation of the proposed method is performed by assessing the Normalized Mean Square Error of predicted values over observed values from a real cloud computing dataset, collected by monitoring the utilization of Dropbox. Compared with other predictors, our solution exhibits the strongest correlation level and shows a close match with real observations.

Abstract
We present a collision-free jammer selection policy for enhanced wireless secrecy. Jammers, selected from the neighbors of a source, are friendly in the sense that they are willing to help the source to transmit securely by causing interference/collisions to possible eavesdroppers. The proposed jammer selection policy results in the selection of the largest number of jammers that do not cause collisions among themselves. This enables jammers to assist the source to transmit securely by causing interference to eavesdroppers, while sending their own traffic into the network. © 2013 IEEE.