Abstract
Context. eta Car is one of the most intriguing luminous blue variables in the Galaxy. Observations and models of the X-ray, ultraviolet, optical, and infrared emission suggest a central binary in a highly eccentric orbit with a 5.54 yr period residing in its core. 2D and 3D radiative transfer and hydrodynamic simulations predict a primary with a dense and slow stellar wind that interacts with the faster and lower density wind of the secondary. The wind-wind collision scenario suggests that the secondary's wind penetrates the primary's wind creating a low-density cavity in it, with dense walls where the two winds interact. However, the morphology of the cavity and its physical properties are not yet fully constrained. Aims. We aim to trace the inner similar to 5-50 au structure of eta Car's wind-wind interaction, as seen through Br gamma and, for the first time, through the He i 2s-2p line. Methods. We have used spectro-interferometric observations with the K-band beam-combiner GRAVITY at the VLTI. The analyses of the data include (i) parametrical model-fitting to the interferometric observables, (ii) a CMFGEN model of the source's spectrum, and (iii) interferometric image reconstruction. Results. Our geometrical modeling of the continuum data allows us to estimate its FWHM angular size close to 2 mas and an elongation ratio epsilon = 1.06 +/- 0.05 over a PA = 130 degrees +/- 20 degrees. Our CMFGEN modeling of the spectrum helped us to confirm that the role of the secondary should be taken into account to properly reproduce the observed Br gamma and He i lines. Chromatic images across the Br gamma line reveal a southeast arc-like feature, possibly associated to the hot post-shocked winds flowing along the cavity wall. The images of the He i 2s-2p line served to constrain the 20 mas (similar to 50 au) structure of the line-emitting region. The observed morphology of He i suggests that the secondary is responsible for the ionized material that produces the line profile. Both the Br gamma and the He i 2s-2p maps are consistent with previous hydrodynamical models of the colliding wind scenario. Future dedicated simulations together with an extensive interferometric campaign are necessary to refine our constraints on the wind and stellar parameters of the binary, which finally will help us predict the evolutionary path of eta Car.

Abstract
This paper presents a reliability-based approach for the design and deployment of an energy management system (EMS) by using 'smart' applications, such as energy storage (ES), to control battery power output in residential dwellings, and thus improve distribution-network reliability performance. The state of charge (SOC) of the battery system is designed based on time-varying electricity tariff, load demand and solar photovoltaic (PV) generation data to investigate a realistic test-case scenario. Additionally, a typical MV/LV urban distribution system is fully modelled and scripted to investigate the potential benefits that 'smart' interventions can offer to customers' quality of power supply. In this research, Monte-Carlo simulation method is further developed to include the time-variation of electricity demand profiles and failure rates of network components. Accordingly, the reliability-based effects from SOC variation in batteries are compared with an uncontrolled microgeneration (MG) scenario, by using different PV penetration levels to justify the value of control. The benefits are assessed through standard reliability indices measuring frequency and duration of power interruptions and most importantly, the energy not supplied to customers during sustained interruptions.

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.