In its quest for approaches to taming uncertainty in self-adaptive systems (SAS), the research community has largely focused on solutions that adapt the SAS architecture or behaviour in response to uncertainty. By comparison, solutions that reduce the uncertainty affecting SAS (other than through the blanket monitoring of their components and environment) remain underexplored. Our previous work proposed Parley , a more nuanced, adaptive approach to SAS uncertainty reduction. To that end, we introduced an SAS architecture comprising an uncertainty reduction controller that drives the adaptive acquisition of new information within the SAS adaptation loop and a tool-supported method that uses probabilistic model checking to synthesise such controllers. The controllers generated by our method deliver optimal tradeoffs between SAS uncertainty reduction benefits and new information acquisition costs with guarantees for the satisfaction of requirements. In this article, we extend Parley to Parley+ by improving the synthesis of these controllers and by expanding the formalisation of Parley+ to prove the validity of the synthesis. We illustrate the use and extend the evaluation of the effectiveness of our approach for mobile robot navigation and service-based system SAS. The evaluation results show that Parley+ can synthesise controllers that help achieve the system’s objectives significantly better than Parley in 88.1% of the cases.

As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this difficult task, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues, such as conflicts, redundancy, restrictiveness, and insufficiency, yielding diagnostics that pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs, comprising 62 issues for the software underpinning the operation of systems, such as, assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.

Robotic systems are becoming pervasive and adopted in increasingly many domains, such as manufacturing, healthcare, and space exploration. To this end, engineering software has emerged as a crucial discipline for building maintainable and reusable robotic systems. The field of robotics software engineering research has received increasing attention, fostering autonomy as a fundamental goal. However, robotics developers are still challenged trying to achieve this goal given that simulation is not able to deliver solutions to realistically emulate real-world phenomena. Robots also need to operate in unpredictable and uncontrollable environments, which require safe and trustworthy self-adaptation capabilities implemented in software. Typical techniques to address the challenges are runtime verification, field-based testing, and mitigation techniques that enable fail-safe solutions. However, there is no clear guidance to architect ROS-based systems to enable and facilitate runtime verification and field-based testing. This paper aims to fill in this gap by providing guidelines that can help developers and quality assurance (QA) teams when developing, verifying or testing their robots in the field. These guidelines are carefully tailored to address the challenges and requirements of testing robotics systems in real-world scenarios. We conducted (i) a literature review on studies addressing runtime verification and field-based testing for robotic systems, (ii) mined ROS-based applications repositories, and (iii) validated the applicability, clarity, and usefulness via two questionnaires with 55 answers overall. We contribute 20 guidelines: 8 for developers and 12 for QA teams formulated for researchers and practitioners in robotic software engineering. Finally, we map our guidelines to open challenges thus far in runtime verification and field-based testing for ROS-based systems and, we outline promising research directions in the field.Guidelines website and replication package:https://ros-rvft.github.io.

We present DeepDECS, a new method for the synthesis of correct-by-construction software controllers for autonomous systems that use deep neural network (DNN) classifiers for the perception step of their decision-making processes. Despite major advances in deep learning in recent years, providing safety guarantees for these systems remains very challenging. Our controller synthesis method addresses this challenge by integrating DNN verification with the synthesis of verified Markov models. The synthesised models correspond to discrete-event software controllers guaranteed to satisfy the safety, dependability and performance requirements of the autonomous system, and to be Pareto optimal with respect to a set of optimisation objectives. We evaluate the method in simulation by using it to synthesise controllers for mobile-robot collision limitation, and for maintaining driver attentiveness in shared-control autonomous driving.

To accurately make adaptation decisions, a self-adaptive system needs precise means to analyze itself at runtime. To this end, runtime verification can be used in the feedback loop to check that the managed system satisfies its requirements formalized as temporal-logic properties. These requirements, however, may change due to system evolution or uncertainty in the environment, managed system, and requirements themselves. Thus, the properties under investigation by the runtime verification have to be dynamically adapted to represent the changing requirements while preserving the knowledge about requirements satisfaction gathered thus far, all with minimal latency. To address this need, we present a runtime verification approach for self-adaptive systems with changing requirements. Our approach uses property specification patterns to automatically obtain automata with precise semantics that are the basis for runtime verification. The automata can be safely adapted during runtime verification while preserving intermediate verification results to seamlessly reflect requirement changes and enable continuous verification. We evaluate our approach on an Arduino prototype of the Body Sensor Network and the Timescales benchmark. Results show that our approach is over five times faster than the typical approach of redeploying and restarting runtime monitors to reflect requirements changes, while improving the system’s trustworthiness by avoiding interruptions of verification.

The price of virtual machine instances in the Amazon EC2 spot model is often much lower than in the on-demand counterpart. However, this price reduction comes with a decrease in the availability guarantees. Several mechanisms have been proposed to analyze the spot model in the last years, employing different strategies. To our knowledge, there is no work that accurately captures the trade-off between spot price and availability, for short term analysis, and does long term analysis for spot price tendencies, in favor of user decision making. In this work, we propose (a) a utility-based strategy, that balances cost and availability of spot instances and is targeted to short-term analysis, and (b) a LSTM (Long Short Term Memory) neural network framework for long term spot price tendency analysis. Our experiments show that, for r4.2xlarge, 90 percent of spot bid suggestions ensured at least 5.73 hours of availability in the second quarter of 2020, with a bid price of approximately 38 percent of the on-demand price. The LSTM experiments were able to predict spot prices tendencies for several instance types with very low error. Our LSTM framework predicted an average value of 0.19 USD/hour for the r5.2xlarge instance type (Mean Squared Error$<10^{-6}$) for a 7-day period of time, which is about 37 percent of the on-demand price. Finally, we used our combined mechanism on an application that compares thousands of SARS-CoV-2 DNA sequences and show that our approach is able to provide good choices of instances, with low bids and very good availability.

In the Amazon EC2 cloud provider, the price of spot instances is much lower than on demand instances, however, at the cost of availability issues of the former. Recently, several strategies were proposed to analyze the Amazon EC2 spot pricing model employing techniques such as statistical and probabilistic modeling and neural networks. To the best of our knowledge, there is no work in the literature that can accurately capture the trade-off between price and availability in favor of user decision-making. In this work, we propose and evaluate a utility-based strategy that balances spot instance cost and availability to Amazon EC2 users. Our experiments show that the average availability reaches up to 98% for spot instances, using data gathered from Amazon (September to November 2016), and a bid value below 28% of the on demand price for the m4.10xlarge general purpose instance type.

Summary Biological sequence comparison is often used as an auxiliary task in the analysis of genetic material. Pairwise comparison algorithms like Smith‐Waterman evaluate two strings representing sequences of proteins, DNA or RNA to obtain optimal alignment between them. Many applications have been proposed to address the sequence comparison problem, prioritizing the use of graphics cards and proprietary languages such as CUDA. In this paper, we propose and evaluate MASA‐OpenCL, an OpenCL solution for comparing long DNA sequences that is based on the MASA sequence alignment framework, with pruning capability proportional to the similarity of the sequences compared. The results of MASA‐OpenCL were compared to its CUDA counterpart (MASA‐CUDAlign) and, in most cases, MASA‐OpenCL achieved better performance. In order to better understand the behavior of MASA‐OpenCL, we performed a statistical analysis considering 11 comparisons of sequences with high, medium and low similarity in 4 GPUs. As a result, we obtained a multiple linear regression model that considers (a) the sizes of the sequences, (b) the similarity between them, (c) the computational power of the GPU, and (d) the GPU memory bandwidth. We used this model to predict the performance in two other GPUs, with low error rates.

Summary In this paper, we conduct statistical analyses for two Amazon cloud pricing models: on demand and spot. On demand cloud instances are charged a fixed price and can only be terminated by the user, with very high availability. On the other hand, spot instances are charged a dynamic price determined by a market‐driven model and can be revoked by the provider when the spot price becomes higher than the user‐defined price, having possibly low availability. Our analysis for on‐demand instances resulted in multiple linear regression equations that represent the influence of characteristics of the processor and RAM memory in the composition of the price of different types of instances available on the Amazon EC2 provider. In order to analyze the Amazon spot pricing, we used time‐smoothed moving averages by 12‐hour periods, aiming to provide a price‐availability trade‐off to the user. Our experiments with spot price histories from September to November 2016 show that the user's bid can be set at 30% of the on‐demand price, with an availability above of 90%, depending on instance type.

Adaptivity is a capability that enables a system to choose amongst various alternatives to satisfy or maintain the satisfaction of certain requirements. The criteria of requirements satisfaction could be pragmatic and context-dependent. Contextual Goal Models (CGM) capture the power of context on banning or allowing certain alternatives to reach requirements (goals) and also deciding the quality of those alternatives with regards to certain quality measures (softgoals). It is used to depict facets of the decision making strategy and rationale of an adaptive system at the preliminary level of requirements. In this paper we argue the case for pragmatic requirements and extend the CGM with additional constructs to capture them and allow their analysis. We also develop an automated analysis which aids the planning and scheduling of tasks execution to meet pragmatic goals. Moreover, we evaluate our modelling and analysis regarding correctness and performance. Such an evaluation showed the applicability of the approach and its usefulness in aiding sensible decisions. It has also shown its capability to do so in a time short enough to suit run-time adaptation decision making.

Software Product Lines (SPLs) are techniques where several artefacts are reused (domain), and some are customised (variation points). An SPL can bind variation points statically (compilation time) or dynamically (runtime). Dynamic Software Product Lines (DSPLs) use dynamic binding to adapt to the environment or requirements changes. DSPLs are commonly used to build dependable systems, defined as systems with the ability to avoid more frequent or severe service failures than the acceptable. The main dependability attributes are availability, confidentiality, integrity, reliability, maintainability, and safety. To better understand this context, a Systematic Mapping Study (SMS) was applied searching proposals that include dependability attributes in DSPLs. Our results suggest that few solutions handle dependability in DSPL context. We selected nine primary studies in this regard. We performed a comparative study of the results, analysing other dimensions, and facets, aiming for a better understanding of this research area.

Nowadays, cloud users face three important problems: (a) choosing one or more appropriate cloud provider(s) to run their application(s), (b) selecting appropriate cloud resources, which implies having enough information about the available resources, including their characteristics and constraints, and (c) configuring the cloud resources. These problems are mostly due to the wide range of resources. These resources usually have distinct dependencies, and they are offered at various clouds' layers. In this complex scenario, the users often have to handle cloud resources and their dependencies manually. This is an error-prone and time-consuming activity, even for skilled cloud users and system administrators. In this context, this paper proposes a software product line engineering (SPLE) method and a tool to deal with these issues. Our SPL-based engineering method enables a declarative and goal-oriented strategy. Furthermore, it allows resource selection and configuration in inter-cloud environments. In our proposal, the cloud users specify their applications and requirements, and our tool automatically selects and configures a suitable computing environment, taking into account temporal and functional dependencies. Experimental results on Amazon EC2 and Google Compute Engine (GCE) show that our approach enables unskilled users to have access to advanced inter-cloud computing configurations, without being concerned with the characteristics of each cloud.

This paper presents a model of the connectivity of a wireless sensor network (WSN) deployed over a square area, which considers border effects. This model supports an accurate evaluation of the reliability of the network with and without node failures. Using the proposed model we analyze the tradeoff between the number of sensors and their communication range when deploying a wireless network that is connected with high probability and validate this analysis through simulation experiments. Additional simulations, considering sensor failures, ratified that periodic sensor redeployments, calculated according to the proposed model, can extend the reliability of WSNs, keeping them connected with high probability. For applications that can withstand temporary network disconnection, we obtained theoretical and experimental evidence that the proposed model also supports the calculation of a less frequent redeployment procedure that provides network connectivity at high levels of availability. Finally, extending the approach to a circular shaped area was considered.

The main contribution of this research is to provide platform-independent means to support reliability design following the principles of a model driven approach. The contribution aims to systematically address dependability concerns from the early to the late stages of software development. MDA appears to be a suitable framework to assess these concerns and, therefore, semantically integrate analysis and design models into one environment.