Abstract
In the area of algebraic specification there are two main approaches for defining observational abstraction: behavioural specifications use a notion of observational satisfaction for the axioms of a specification, whereas abstractor specifications define an abstraction from the standard semantics of a specification w.r.t. an observational equivalence relation between algebras. Earlier work by Bidoit, Hennicker, Wirsing has shown that in the case of first-order logic specifications both concepts coincide semantically under mild assumptions. Analogous results have been shown by Sannella and Hofmann for higher-order logic specifications and recently, by Hennicker and Madeira, for specifications of reactive systems using a dynamic logic with binders. In this paper, we bring these results into a common setting: we isolate a small set of characteristic principles to express the behaviour/abstractor equivalence and show that all three mentioned specification frameworks satisfy these principles and therefore their behaviour and abstractor specifications coincide semantically (under mild assumptions). As a new case we consider observational modal logic where observational satisfaction of Hennessy-Milner logic formulae is defined "up to" silent transitions and observational abstraction is defined by weak bisimulation. We show that in this case the behaviour/abstractor equivalence can only be obtained, if we restrict models to weakly deterministic labelled transition systems.

Abstract
The K framework is a rewrite logic-based framework for defining programming language semantics suitable for formal reasoning about programs and programming languages. In this paper, we present K-Taint, a rewriting logic-based executable semantics in the K framework for taint analysis of an imperative programming language. Our K semantics can be seen as a sound approximation of programs semantics in the corresponding security type domain. More specifically, as a foundation to this objective, we extend to the case of taint analysis the semantically sound flow-sensitive security type system by Hunt and Sands's, considering a support to the interprocedural analysis as well. With respect to the existing methods, K-Taint supports context- and flow-sensitive analysis, reduces false alarms, and provides a scalable solution. Experimental evaluation on several benchmark codes demonstrates encouraging results as an improvement in the precision of the analysis.

Abstract
The peripheral arterial disease (PAD) is characterized by leg pain during walking, and a recommended treatment for this disease is to perform supervised physical activity. In this chapter, a system that monitories the physical activity containing one application for smartwatch, one application for smartphone, and a back-end webservice is presented. The applications collect heart rate, GPS locations, step count, and altitude data. The methodology used for the development of the system was based on the agile method with the production of prototypes. In this chapter, four development cycles, which cover the users' and researchers' needs, are presented. In this work, the main objective is to evaluate the current mobile technologies on the physical activity data collection and the development of a system that assists the users to maintain an active life. © 2018, IGI Global.

Abstract
A large quantity of variable renewable energy sources (RESs), most notably wind and solar, is now connected to the Portuguese network system, which makes it somehow unique. Yet, in the coming years, the network is expected to accommodate more of these and other technologies of "clean" power productions. The deployment and efficient utilization of various flexibility options are certainly required in a system experiencing such levels of dynamic changes so as to ensure a standard level of service provision in terms of security, stability and reliability. Among these is a battery energy storage system (BESS), which is emerging as one of the most viable and effective options of increasing the much-needed flexibility in power systems. This work aims to assess the impact of deploying BESSs on the operational performance of the Portuguese transmission grid, mainly in terms operational flexibility and variable RES power support. In particular, the potential benefits of strategically placed BESSs are investigated using a stochastic optimization framework. Numerical results show that integrating BESSs leads to a more efficient use of renewable power by considerably minimizing curtailments, and a 10% reduction in system-wide cost. Energy losses are moderately increased as a result of the BESS deployment. But this is offset by the savings in operation and emission costs.

Abstract
The present work aims at the development of a new heuristic approach named Direct-DRRT . This new algorithm is an improvement of the DRRT* method, which is the fusion between RRT * and DRRT. This improvement aims at the mobile robot autonomous planning considering less memory and computational time for a route design. The results show the efficiency of our approach compared to the other methods, presenting less processing time and a signification reduced number of nodes and paths. © 2018 IEEE.

Abstract
The irregular strip packing problem consists of cutting a set of convex and non-convex two-dimensional polygonal pieces from a board with a fixed height and infinite length. Owing to the importance of this problem, a large number of mathematical models and solution methods have been proposed. However, only few papers consider that the pieces can be rotated at any angle in order to reduce the board length used. Furthermore, the solution methods proposed in the literature are mostly heuristic. This paper proposes a novel mixed integer quadratically-constrained programming model for the irregular strip packing problem considering continuous rotations for the pieces. In the model, the pieces are allocated on the board using a reference point and its allocation is given by the translation and rotation of the pieces. To reduce the number of symmetric solutions for the model, sets of symmetry-breaking constraints are proposed. Computational experiments were performed on the model with and without symmetry-breaking constraints, showing that symmetry elimination improves the quality of solutions found by the solution methods. Tests were performed with instances from the literature. For two instances, it was possible to compare the solutions with a previous model from the literature and show that the proposed model is able to obtain numerically accurate solutions in competitive computational times.