Abstract: This paper presents Fortis, a tool for automated, formal analysis and repair of robust discrete systems. Given a system model, an environment model, and a safety property, the tool can be used to automatically compute robustness as the amount of deviations in the environment under which the system can continue to guarantee the property. In addition, Fortis enables automated repair of a given system to improve its robustness against a set of intolerable deviations through a process called robustification. With these techniques, Fortis enables a new process for developing robust-by-design systems. The paper presents the overall design of Fortis as well as the key details behind the robustness analysis and robustification techniques. The applicability and performance of Fortis are illustrated through experimental results over a set of case study systems, including a radiation therapy system, an electronic voting machine, network protocols, and a transportation fare system.

Abstract: The feature interaction problem occurs when two or more independently developed components interact with each other in unanticipated ways, resulting in undesirable system behaviors. Feature interaction problems remain a challenge for emerging domains in cyber-physical systems (CPS), such as the Internet of Things and autonomous drones. Existing techniques for resolving feature interactions take a “winner-takes-all” approach, where one out of the conflicting features is selected as the most desirable one, and the rest are disabled. However, when multiple of the conflicting features fulfill important system requirements, being forced to select one of them can result in an undesirable system outcome. In this paper, we propose a new resolution approach that allows all of the conflicting features to continue to partially fulfill their requirements during the resolution process. In particular, our approach leverages the idea of adaptive requirement weakening, which involves one or more features temporarily weakening their level of performance in order to co-exist with the other features in a consistent manner. Given feature requirements specified in Signal Temporal Logic (STL), we propose an automated method and a runtime architecture for automatically weakening the requirements to resolve a conflict. We demonstrate our approach through case studies on feature interactions in autonomous drones.

Abstract: Modern software systems are deployed in a highly dynamic, uncertain environment. Ideally, a system that is robust should be capable of establishing its most critical requirements even in the presence of possible deviations in the environment. We propose a technique called behavioral robustification, which involves systematically and rigorously improving the robustness of a design against potential deviations. Given behavioral models of a system and its environment, along with a set of user-specified deviations, our robustification method produces a redesign that is capable of satisfying a desired property even when the environment exhibits those deviations. In particular, we describe how the robustification problem can be formulated as a multi- objective optimization problem, where the goal is to restrict the deviating environment from causing a violation of a desired property, while maximizing the amount of existing functionality and minimizing the cost of changes to the original design. We demonstrate the effectiveness of our approach on case studies involving the robustness of an electronic voting machine and safety-critical interfaces.

Abstract: Self-adaptive systems typically operate in heterogeneous environments and need to optimize their behavior based on a variety of quality attributes to meet stakeholders' needs. During adaptation planning, these quality attributes are considered in the form of constraints, describing requirements that must be fulfilled, and utility functions, which are used to select an optimal plan among several alternatives. Up until now, most automated planning approaches are not designed to adapt quality attributes, their priorities, and their trade-offs at run time. Instead, both utility functions and constraints are commonly defined at design time. There exists a clear lack of run-time mechanisms that support their adaptation in response to changes in the environment or in stakeholders' preferences. In this paper, we present initial work that combines automated planning and adaptation of quality attributes to address this gap. The approach helps to semi-automatically adjust utility functions and constraints based on changes at run time. We present a preliminary experimental evaluation that indicates that our approach can provide plans with higher utility values while fulfilling changed or added constraints. We conclude this paper with our envisioned research outlook and plans for future empirical studies.