Abstract
The IEC 61499 standard proposes an event driven execution model for component based (in terms of Function Blocks), distributed industrial automation applications. However, the standard provides only an informal execution semantics, thus in consequence behavior and correctness relies on the design decisions made by the tool vendor. In this paper we present the formalization of a subset of the IEC 61499 standard in order to provide an underpinning for the static verification of Function Block models by means of deductive reasoning. Specifically, we contribute by addressing verification at the component, algorithm, and ECC levels. From Function Block descriptions, enriched with formal contracts, we show that correctness of component compositions, as well as functional and transitional behavior can be ensured. Feasibility of the approach is demonstrated by manually encoding a set of representative use-cases in WhyML, for which the verification conditions are automatically derived (through the Why3 platform) and discharged (using automatic SMT-based solvers). Furthermore, we discuss opportunities and challenges towards deriving certified executables for IEC 61499 models. © 2016 IEEE.

Abstract
Hierarchical Data Format (HDF5) is a popular binary storage solution in high performance computing (HPC) and other scientific fields. It has bindings for many popular programming languages, including C++, which is widely used in the HPC field. Its C++ API requires mapping of the native C++ data types to types native to the HDF5 API. This task can be error prone, especially when working with complex data structures, which are usually stored using HDF5 compound data types. Due to the lack of a comprehensive reflection mechanism in C++, the mapping code for data manipulation has to be hand-written for each compound type separately. This approach is vulnerable to bugs and mistakes, which can be eliminated by using an automated code generation phase. In this paper we present an approach implemented in the LARA language and supported by the tool Clava, which allows us to automate the generation of the HDF5 data access code for complex data structures in C++.

Abstract
This paper presents a methodology for forecasting the average downlink throughput for an LTE cell by using real measurement data collected by multiple LTE probes. The approach uses data analytics techniques, namely forecasting algorithms to anticipate cell congestion events which can then be used by Self-Organizing Network (SON) strategies for triggering network re-configurations, such as shifting coverage and capacity to areas where they are most needed, before subscribers have been impacted by dropped calls or reduced data speeds. The presented implementation results show the prediction of network behaviour is possible with a high level of accuracy, effectively allowing SON strategies to be enforced in time.

Abstract
The main goal of this paper is to present a set of well-defined and structured procedures to establish guidelines for the application of an integrated assessment of energy performance and indoor climate in schools. Increasing the knowledge about how energy is consumed in schools is a way to enhance the awareness of school managers (board of directors) about the importance of improving energy efficiency and reducing energy costs. The proposed methodology helps to identify major energy consuming equipment in school buildings and potential energy conservation measures. The assessment of indoor climate identifies potential corrective measures to problems related to indoor air quality and thermal comfort, also supporting the study of further energy conservation measures associated with ensuring environmental quality. Results of a case study showed that the expected energy consumption reduction is about 11.2% due to a better usage of daylighting and 4.5% due to the reduction of fresh air flow rates, while extending the ventilation operation time. In addition, there is a considerable non-calculated potential for energy savings and improvement of indoor environmental conditions in school buildings, promoting students and teachers productivity and wellbeing.

Abstract
Micromachining with femtosecond laser can be exploited to fabricate optical components and microfluidic channels in fused silica, due to internal modification of the glass properties that is induced by the laser beam. In this paper, we refer to the formation of microfluidic channels, where an optimization of the fabrication procedure was conducted by examining etch rate and surface roughness as a function of the irradiation conditions. Microfluidic channels with high and uniform aspect ratio and with smooth sidewalls were obtained, and such structures were successfully integrated with optical components. The obtained results set the foundations towards the development of new optofluidic devices.

Abstract
Major rivers have traditionally been linked with important human settlements throughout history. The growth of cities over recent river deposits makes necessary the use of multidisciplinary approaches to characterize the evolution of drainage networks in urbanized areas. Since under-consolidated fluvial sediments are especially sensitive to compaction, their spatial distribution, thickness, and mechanical behavior must be studied. Here, we report on subsidence in the city of Seville (Southern Spain) between 2003 and 2010, through the analysis of the results obtained with the Multi-Temporal InSAR (MT-InSAR) technique. In addition, the temporal evolution of the subsidence is correlated with the rainfall, the river water column and the piezometric level. Finally, we characterize the geotechnical parameters of the fluvial sediments and calculate the theoretical settlement in the most representative sectors. Deformation maps clearly indicate that the spatial extent of subsidence is controlled by the distribution of under-consolidated fine-grained fluvial sediments at heights comprised in the range of river level variation. This is clearly evident at the western margin of the river and the surroundings of its tributaries, and differs from rainfall results as consequence of the anthropic regulation of the river. On the other hand, this influence is not detected at the eastern margin due to the shallow presence of coarse-grain consolidated sediments of different terrace levels. The derived results prove valuable for implementing urban planning strategies, and the InSAR technique can therefore be considered as a complementary tool to help unravel the subsidence tendency of cities located over under-consolidated fluvial deposits. Copyright (c) 2017 John Wiley & Sons, Ltd.