Abstract
Verification and testing are two of the most costly and time consuming steps during the development of safety critical systems. The advent of complex and sometimes partially unpredictable computing architectures such as multicore commercial-of-the-shelf platforms, together with the composable development approach adopted in multiple industrial domains such as avionics and automotive, rendered the exhaustive testing of all situations that could potentially be encountered by the system once deployed on the field nearly impossible. Run-time verification (RV) is a promising solution to help accelerate the development of safety critical applications whilst maintaining the high degree of reliability required by such systems. RV adds monitors in the application, which check at run-time if the system is behaving according to predefined specifications. In case of deviations from the specifications during the runtime, safeguarding measures can be triggered in order to keep the system and its environment in a safe state, as well as potentially attempting to recover from the fault that caused the misbehaviour. Most of the state-of-the-art on RV essentially focused on the monitor generation, concentrating on the expressiveness of the specification language and its translation in correct-by-construction monitors. Few of them addressed the problem of designing an efficient and safe run-time monitoring (RM) architecture. Yet, RM is a key component for RV. The RM layer gathers information from the monitored application and transmits it to the monitors. Therefore, without an efficient and safe RM architecture, the whole RV system becomes useless, as its inputs and hence by extension its outputs cannot be trusted. In this paper, we discuss the design of a novel RM architecture suited to safety critical applications. © Springer International Publishing Switzerland 2015.

Abstract
Several real world prediction problems involve forecasting rare values of a target variable. When this variable is nominal, we have a problem of class imbalance that was thoroughly studied within machine learning. For regression tasks, where the target variable is continuous, few works exist addressing this type of problem. Still, important applications involve forecasting rare extreme values of a continuous target variable. This paper describes a contribution to this type of tasks. Namely, we propose to address such tasks by resampling approaches that change the distribution of the given data set to decrease the problem of imbalance between the rare target cases and the most frequent ones. We present two modifications of well-known resampling strategies for classification tasks: the under-sampling and the synthetic minority over-sampling technique (SMOTE) methods. These modifications allow the use of these strategies on regression tasks where the goal is to forecast rare extreme values of the target variable. In an extensive set of experiments, we provide empirical evidence for the superiority of our proposals for these particular regression tasks. The proposed resampling methods can be used with any existing regression algorithm, which means that they are general tools for addressing problems of forecasting rare extreme values of a continuous target variable.

Abstract
Hierarchical transition systems provide a popular mathematical structure to represent state-based software applications in which different layers of abstraction are represented by inter-related state machines. The decomposition of high level states into inner sub-states, and of their transitions into inner sub-transitions is common refinement procedure adopted in a number of specification formalisms. This paper introduces a hybrid modal logic for k-layered transition systems, its first-order standard translation, a notion of bisimulation, and a modal invariance result. Layered and hierarchical notions of refinement are also discussed in this setting.

Abstract
The process of visually exploring underwater environments is still a complex problem. Underwater vision systems require complementary means of sensor information to help overcome water disturbances. This work proposes the development of calibration methods for a structured light based system consisting on a camera and a laser with a line beam. Two different calibration procedures that require only two images from different viewpoints were developed and tested in dry and underwater environments. Results obtained show, an accurate calibration for the camera/projector pair with errors close to 1 mm even in the presence of a small stereos baseline.

Abstract
A coordinated strategy between wind and reversible hydro units for the midterm planning that reduces the imbalance of wind power and improves system efficiency is proposed. A stochastic mixed integer linear model is used, which maximizes the joint profit of wind and hydro units, where conditional value at risk (CVaR) is used for model risk. The offering strategies studied are 1) separate wind and hydro pumping offer, where the units work separately without a physical connection and 2) a single wind and hydro pumping offer with a physical connection between them to store wind energy for future use. The effects of a coordinated wind-hydro strategy for midterm planning are analyzed, considering CVaR and the future water value. The future water value in the reservoirs is analyzed hourly for a period of 1 week and 2 months, in two realistic case studies.

Abstract
This paper presents an algorithm for integrating and managing electrochemical energy storage systems (ESSs) on unit commitment (UC) problem. As some elements required for integrating electrochemical ESS, such as the power converter, have non-linear characteristics, its corresponding linear modeling could be difficult to be developed and included on the UC problem, which could lead to unfeasible solutions or unexpected results. In order to incorporate full models of ESS and its interface with the power system, in this paper an algorithm to incorporate electrochemical ESS management on the UC problem is presented. An insular power system of 10-units is analyzed, and conclusions are duly drawn.