Abstract
Although hardware is generally seen as the main culprit for a computer's energy usage, software too has a tremendous impact on the energy spent. Unfortunately, there is still not enough support for software developers so they can make their code more energy-aware. This paper proposes a technique to detect energy inefficient fragments in the source code of a software system. Test cases are executed to obtain energy consumption measurements, and a statistical method, based on spectrum-based fault localization, is introduced to relate energy consumption to the source code. The result of our technique is an energy ranking of source code fragments pointing developers to possible energy leaks in their code. This technique was implemented in the SPELL toolkit. Finally, in order to evaluate our technique, we conducted an empirical study where we asked participants to optimize the energy efficiency of a software system using our tool, while also having two other groups using no tool assistance and a profiler, respectively. We showed statistical evidence that developers using our technique were able to improve the energy efficiency by 43% on average, and even out performing a profiler for energy optimization.

Abstract
This study studies a double-surface sliding-mode observer (DS-SMO) for estimating the flux and speed of induction motors (IMs). The SMO equations are based on an IM model in the stationary reference frame. The DS-SMO is developed based on the equations of a single-surface SMO (SS-SMO) of IM. In DS-SMO method, the observer is designed through combining sliding variables produced by combining estimated fluxes of currents error. The speed is easily determined based on the pass of switching signal through a low-pass filter. Also, an optimal DS-SMO (ODS-SMO) is proposed to improve the transient condition by optimally tuning the observer parameters. To optimise these parameters, the particle swarm optimisation method is adopted. Moreover, an improved DS-SMO (IDS-SMO) is proposed to improve both transient and steady-state conditions, torque ripple and total harmonic distortion. Moreover, the proposed IDS-SMO has a stable performance under sudden load change and the low-speed region. Finally, the accuracy of the proposed ODS-SMO and IDS-SMO methods is substantiated through simulation and experimental results.

Abstract
We extend dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations of the logic: abstractor and behavioural specifications. Abstractor specifications relax the standard model class semantics of a specification by considering its closure under weak bisimulation. Behavioural specifications, however, rely on a behavioural satisfaction relation which relaxes the interpretation of state variables and the satisfaction of modal formulas phi and [alpha]phi by abstracting from silent transitions. A formal relation between abstractor and behavioural specifications is provided which shows that both coincide semantically under mild conditions. For the proof we instantiate the previously introduced concept of a behaviour-abstractor framework to the case of dynamic logic with binders and silent transitions.

Abstract
Tensor-based models emerged only recently in modeling and analysis of the spatiotemporal road traffic data. They outperform other data models regarding the property of simultaneously capturing both spatial and temporal components of the observed traffic dataset. In this paper, the nonnegative tensor decomposition method is used to extract traffic patterns in the form of Speed Transition Matrix (STM). The STM is presented as the approach for modeling the large sparse Floating Car Data (FCD). The anomaly of the traffic pattern is estimated using Kullback–Leibler divergence between the observed traffic pattern and the average traffic pattern. Experiments were conducted on the large sparse FCD dataset for the most relevant road segments in the City of Zagreb, which is the capital and largest city in Croatia. Results show that the method was able to detect the most anomalous traffic road segments, and with analysis of the extracted spatial and temporal components, conclusions could be drawn about the causes of the anomalies. Results are validated by using the domain knowledge from the Highway Capacity Manual and achieved a precision score value of more than 90%. Therefore, such valuable traffic information can be used in routing applications and urban traffic planning. © 2020, Springer Nature Switzerland AG.

Abstract
Robots are currently deployed in safety-critical domains but proper techniques to assess the functional safety of their software are yet to be adopted. This is particularly critical in ROS, where highly configurable robots are built by composing third-party modules. To promote adoption, we advocate the use of lightweight formal methods, automatic techniques with minimal user input and intuitive feedback. This paper proposes a technique to automatically verify system-wide safety properties of ROS-based applications at static time. It is based in the formalization of ROS architectural models and node behaviour in Electrum, over which system-wide specifications are subsequently model checked. To automate the analysis, it is deployed as a plug-in for HAROS, a framework for the assessment of ROS software quality aimed at the ROS community. The technique is evaluated in a real robot, AgRob V16, with positive results.

Abstract
The aim of this chapter focuses on featuring firmed IoT architecture paradigms and advocating, knowingly in concrete use cases, the combined use of such architecture categories. It is common knowledge that the growing demand for embedded processing, interconnection, and integration facilities in everyday objects is being driven by a multitude of IoT projects. The smart cities, smart agriculture, manufacturing, and industrial automation areas are some of the most important application grounds. Equally important is the medical sector where specially framed in this publication, the personal home healthcare scenarios gain enormous relevance due to the potential of IoT technology application. It is also becoming clear that the IoT-trending efforts are compelling researchers into the concurrent combination of multiple IoT-computing architecture types or paradigms, to know: wide-range cloud-computing architectures, local-spread fog-computing architectures, and spottily scattered edge-computing architectures. This chapter focuses on identifying the major goals and benefits of each of these architectures classes; describing the relevant state of the art projects, which apply such architecture categories in home healthcare settings; and finally, pinpointing our own experience with home e-health demonstrative use case scenarios, where the benefits of using each of these architecture types become evident, and the concurrent combination of such IoT architectures inevitable. © 2021 Elsevier Inc.