Abstract
Robotic technologies are continuously transforming the domestic and the industrial environments. Recently the Robotic Operating System (ROS), has been widely adopted both by industry and academia, becoming one of the most popular middleware frameworks for developing robot applications. Guaranteeing the correct behaviour of robotic systems is, however, challenging due to their potential for parameterization and heterogeneity. Although different approaches exist, focusing on concrete domain spaces for specific scenarios, no general approach to reason about ROS systems has yet arisen. This paper proposes an approach to model and verify ROS systems using real time properties, focusing on one of the main features of ROS, the communication between nodes. It takes low-level parameters into account, such as queue sizes and timeouts, and uses timed automata as the modelling language. The robot Kobuki is used as a complex case study, over which properties are automatically verified using the UPPAAL model checker, enabling the identification of problematic parameter combinations.

Abstract
The safety-critical real-time embedded domain increasingly demands the use of parallel architectures to fulfill performance requirements. Such architectures require the use of parallel programming models to exploit the underlying parallelism. This paper evaluates the applicability of using OpenMP, a widespread parallel programming model, with Ada, a language widely used in the safety-critical domain. Concretely, this paper shows that applying the OpenMP tasking model to exploit fine-grained parallelism within Ada tasks does not impact on programs safeness and correctness, which is vital in the environments where Ada is mostly used. Moreover, we compare the OpenMP tasking model with the proposal of Ada extensions to define parallel blocks, parallel loops and reductions. Overall, we conclude that the OpenMP tasking model can be safely used in such environments, being a promising approach to exploit fine-grain parallelism in Ada tasks, and we identify the issues which still need to be further researched.

Abstract
The development of economical optical devices with a reduced footprint foreseeing manipulation, sorting and detection of single cells and other micro particles have been encouraged by cellular biology requirements. Nonetheless, researchers are still ambitious for advances in this field. This paper presents Fresnel zone and phase plates fabricated on mode expanded optical fibres for optical trapping. The diffractive structures were fabricated using focused ion beam milling. The zone plates presented in this work have focal distance of similar to 5 mu m, while the focal distance of the phase plates is similar to 10 mu m. The phase plates are implemented in an optical trapping configuration, and 2D manipulation and detection of 8 mu m PMMA beads and yeast cells is reported. This enables new applications for optical trapping setups based on diffractive optical elements on optical fibre tips, where feedback systems can be integrated to automatically detect, manipulate and sort cells.

Abstract
In this paper we discuss the development of a fast ray-tracing solver for complex anisotropic uniaxial optical media based on heterogeneous supercomputing in GPGPU using PyOpenCl. This solver simulates both the propagation of ordinary and extraordinary rays, while taking into account the polarization rotation introduced by position dependent modulations of the optical axis of the medium. We demonstrate the application of this solver by simulating the generation of polarization caustics in random uniaxial optical media.

Abstract
Context: Software testing is an important task in software product quality assurance. Alternatives approach for teaching and training students and professionals have been addressed in many studies, recently. In this article, peer testing is investigated as one alternative approach to mitigate the current lack of well-trained professionals. Objective: To verify the efficiency and efficacy of peer testing in order to create test cases to promote software testing education and training. Method: Conduct a controlled experiment in which subjects design and implement test cases for three small software units. Results and conclusions: In this study, it has been observed that peer testing was significantly more efficient than individual testing (with t-Test). On the other hand, it has not been observed significant differences in the efficacy of peer testing.

Abstract
Measuring the return on communication investments on social media has become one of the top key issues for organizations joining social networks. However, this field has been lacking articulation between what is conveyed as social media key performance indicators and the alignment of strategic organizational goals. Therefore, we propose a methodology to measure the performance of each organization on social media, to determine their positioning in the sector and to evaluate which are the content strategies used to boost the highest performing organizations. Thus, we identify how to determine which organizations should be closely monitored within the sector and which type content strategies can foster higher organizational performance on social media.