Abstract
The integrated use of multiple Synthetic Aperture Radar (SAR) platforms for the deformation monitoring via satellite radar interferometry offers several perspectives for investigation of the behaviour of new and ageing structures, such as buildings and infrastructures, under varying or hazardous environment. Spanning almost 24 years of space-borne radar observations, this study aims to perform classical PSInSAR (Persistent Scatterer Interferometric Synthetic Aperture Radar) analysis incorporating measurements of ERS, Envisat, TerraSAR-X, Sentinel-1A and Radarsat-2 satellites. The results from the processing of different sensing geometries over Bratislava (Slovakia) urban area are presented, focusing on the description of characteristics associated with the specifics of every satellite platform in use. The discussion over technical feasibility of infrastructure monitoring is accompanied by the outline of possible future needs for the utilisation of the wealth source of information provided by the satellite radar imagery. (C) 2016 The Authors. Published by Elsevier B.V.

Abstract
With the increasing importance of software in the aerospace field, as evidenced by its growing size and complexity, a rigorous and reliable software verification and validation process must be applied to ensure conformance with the strict requirements of this software. Although important, traditional validation activities such as testing and simulation can only provide a partial verification of behavior in critical real-time software systems, and thus, formal verification is an alternative to complement these activities. Two useful formal software verification approaches are deductive verification and abstract interpretation, which analyze programs statically to identify defects. This paper explores abstract interpretation and deductive verification by employing Frama-C's value analysis and Jessie plug-ins to verify embedded aerospace control software. The results indicate that both approaches can be employed in a software verification process to make software more reliable.

Abstract
This research aims at tackling a real-world long-haul freight transportation problem where tractors are allowed to exchange semi-trailers through several transshipment points until a request reaches its destiny. The unique characteristics of the considered logistics network allow for providing long-haul services by means of short-haul jobs, drastically reducing empty truck journeys. A greater flexibility is achieved with faster responses. Furthermore, the planning goals as well as the nature of the considered trips led to the definition of a new problem, the long-haul freight transportation problem with multiple transshipment locations. A novel mathematical formulation is developed to ensure resource synchronization while including realistic features, which are commonly found separately in the literature. Considering the complexity and dimension of this routing and scheduling problem, a mathematical programming heuristic (matheuristic) is developed with the objective of obtaining good quality solutions in a reasonable amount of time, considering the logistics business context. We provide a comparison between the results obtained for 79 real-world instances. The developed solution method is now the basis of a decision support system of a Portuguese logistics operator (LO).

Abstract
A number of High Dynamic Range (HDR) video compression algorithms proposed to date have either been developed in isolation or only-partially compared with each other. Previous evaluations were conducted using quality assessment error metrics, which for the most part were developed for qualitative assessment of Low Dynamic Range (LDR) videos. This paper presents a comprehensive objective and subjective evaluation conducted with six published HDR video compression algorithms. The objective evaluation was undertaken on a large set of 39 HDR video sequences using seven numerical error metrics namely: PSNR, logPSNR, puPSNR, puSSIM, Weber MSE, HDR-VDP and HDR-VQM. The subjective evaluation involved six short-listed sequences and two ranking-based subjective experiments with hidden reference at two different output bitrates with 32 participants each, who were tasked to rank distorted HDR video footage compared to an uncompressed version of the same footage. Results suggest a strong correlation between the objective and subjective evaluation. Also, non-backward compatible compression algorithms appear to perform better at lower output bit rates than backward compatible algorithms across the settings used in this evaluation.

Abstract
In this paper an analysis of MicroFactory is carried out and its potential for generating a diversified set of didactic experiences is evaluated. MicroFactory is a robotic competition based on a previously existing competition called Robot@Factory. Robot@Factory is a Portuguese robotic competition whose first edition was held in 2011 in Lisbon. The scenario of the competition simulates a factory which has two warehouses, and eight processing machines. The flow of the materials inside the factory starts at the Incoming Warehouse and ends at the Outgoing Warehouse, eventually passing through one or more processing machines. The robots must collect, transport and position the materials along the process, having to self-localize and navigate while avoiding collisions with walls, obstacles and other robots. There is the option of following predefined tracks present on the floor to ease the navigation problem. Robot@Factory poses challenges like dynamic task scheduling, robot cooperation, trajectory planning, robot navigation with obstacle avoidance, robot self-localization and materials identification and manipulation. Related research contributes to improve AGVs (Automated Guided Vehicle systems) technology. Presently this competition is integrated in Festival Nacional de Robotica, a yearly event which attracts lots of public, contributing also to STEM (Science, Technology, Engineering and Mathematics) popularization. MicroFactory was conceived to be low-cost and easily implementable in a small space, be it a classroom or the school robotics club. The ground area of the factory scenario was reduced to approximately one ninth of its original value. The scenario materials were simplified -the floor is now an A0 printed sheet and the warehouses and machines dimensions are so that they can be 3D printed or made out of LEGO (TM) bricks; both machines and parts had active elements with LEDs and now they are passive. Besides the competition scenario it was also conceived a prototype robot for the competition. It's a 3D printed robot, based on an Arduino board and accessible electronic parts. The creation of this competition is part of a wider Open Source project, aiming to develop project-based collaborative didactic experiences involving robotics and low-cost 3D printed educational robots based on generic electronics to support those experiences. Currently efforts are being dedicated to the inclusion of more sensors in the competition robot, namely low-cost distance sensors and a weight sensor at the claws, the inclusion of different kinds of motors, the development of a new version of the robot incorporating a Raspberry Pi board, the development of a very precise robot localization system, and the conception of a diversified set of didactic experiences based on the MicroFactory competition. This article presents an analysis of MicroFactory and of its inherent challenges. Through this analysis it will be possible to identify topics that can be taught and learned while developing robots to participate in the competition, and to collect elements that will be very useful in the planning and implementation of didactic experiences that work those topics.

Abstract
This paper proposes a new open-loop and low complexity (small size) fast-lock synchronization circuit for clock and data recovery in wearable systems. The system includes sensors embedded in textile and connected by conductive yarns. Synchronization is based on the open-loop selection of the correct phase of the receiver clock synchronously with the incoming signal. The clock generator of the receiver is an autonomous oscillator set to operate at the same nominal frequency. The circuit lock time is at most one clock cycle, faster than all methods based on phase-locked loops or delay-locked loops. The circuit can be used for baseband communication independently of the signal coding method used in the physical layer, making it suitable for many applications. The fully digital circuit (including non-return-to-zero inverted decoder) occupies 0.0022 in a 0.35 complementary metal-oxide semiconductor (CMOS) process, a smaller implementation than many existing circuits, and supports a maximum system clock frequency of 70 for a 35-data rate. Experimental results demonstrate that the proposed circuit robustly generates a synchronous clock for data recovery. The circuit is suitable for systems that tolerate some jitter but requires fast lock time, small size, and low energy consumption. Copyright (c) 2015 John Wiley & Sons, Ltd.