Abstract: Software systems are composed of interacting processes that share data between each other in order to satisfy system properties. When these processes deviate and are unavailable to transmit data—due to events such as software bugs, hardware failures, or security attacks—a resilient system will continue delivering safety-critical services. Identify- ing the processes required to satisfy system properties is not a trivial task as there may exist multiple alternative dataflow paths that each satisfy the property. In this work, we propose a formal modeling and analysis technique to compute the sets of minimal processes required to satisfy dataflow properties. The computation of these sets is reduced to a maximum satisfiability problem via modeling in AlloyMax, a for- mal modeling language that performs bounded model checking. We then present a method to formally define the resilience criteria for a system by constraining the minimal dataflow required under maximum system deviations. The efficacy of this work is then evaluated with four case studies motivated from real-world systems with promising results.
Abstract: Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime monitoring. Given a set of positive and negative examples, specified as traces, LTL learning is the problem of synthesizing a specification, in linear temporal logic (LTL), that evaluates to true over the positive traces and false over the negative ones. In this paper, we propose a new type of LTL learning problem called constrained LTL learning, where the user, in addition to positive and negative examples, is given an option to specify one or more constraints over the properties of the LTL formula to be learned. We demonstrate that the ability to specify these additional constraints significantly increases the range of applications for LTL learning, and also allows efficient generation of LTL formulas that satisfy certain desirable properties (such as minimality). We propose an approach for solving the constrained LTL learning problem through an encoding in first-order relational logic and reduction to an instance of the maximal satisfiability (MaxSAT) problem. An experimental evaluation demonstrates that ATLAS, an implementation of our proposed approach, is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in LTL learning.
Abstract: Cyber-physical systems (CPS) with reinforcement learning (RL)-based controllers are increasingly being deployed in complex phys- ical environments such as autonomous vehicles, the Internet-of-Things (IoT), and smart cities. An important property of a CPS is tolerance; i.e., its ability to function safely under possible disturbances and un- certainties in the actual operation. In this paper, we introduce a new, expressive notion of tolerance that describes how well a controller is ca- pable of satisfying a desired system requirement, specified using Signal Temporal Logic (STL), under possible deviations in the system. Based on this definition, we propose a novel analysis problem, called the tol- erance falsification problem, which involves finding small deviations that result in a violation of the given requirement. We present a novel, two- layer simulation-based analysis framework and a novel search heuristic for finding small tolerance violations. To evaluate our approach, we con- struct a set of benchmark problems where system parameters can be configured to represent different types of uncertainties and disturbances in the system. Our evaluation shows that our falsification approach and heuristic can effectively find small tolerance violations.
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: Alloy is a declarative modeling language based on a first-order relational logic. Its constraint-based analysis has enabled a wide range of applications in software engineering, including configuration synthesis, bug finding, test-case generation, and security analysis. Certain types of analysis tasks in these domains involve finding an optimal solution. For example, in a network configuration problem, instead of finding any valid configuration, it may be desirable to find one that is most permissive (i. e., it permits a maximum number of packets). Due to its dependence on SAT, however, Alloy cannot be used to specify and analyze these types of problems. We propose AlloyMax, an extension of Alloy with a capability to express and analyze problems with optimal solutions. AlloyMax introduces (1) a small addition of language constructs that can be used to specify a wide range of problems that involve optimality and (2) a new analysis engine that leverages a Maximum Satisfiability (MaxSAT) solver to generate optimal solutions. To enable this new type of analysis, we show how a specification in a first-order relational logic can be translated into an input format of MaxSAT solvers - namely, a Boolean formula in weighted conjunctive normal form (WCNF). We demonstrate the applicability and scalability of AlloyMax on a benchmark of problems. To our knowledge, AlloyMax is the first approach to enable analysis with optimality in a relational modeling language, and we believe that AlloyMax has the potential to bring a wide range of new applications to Alloy.
Abstract: Software systems are designed and implemented with assumptions about the environment. However, once the system is deployed,the actual environment may deviate from its expected behavior,possibly undermining desired properties of the system. To enable systematic design of systems that are robust against potential environmental deviations, we propose a rigorous notion of robustness for software systems. In particular, the robustness of a system is de-fined as the largest set of deviating environmental behaviors under which the system is capable of guaranteeing a desired property. We describe a new set of design analysis problems based on our notion of robustness, and a technique for automatically computing robustness of a system given its behavior description. We demonstrate potential applications of our robustness notion on two case studies involving network protocols and safety-critical interfaces.
David Garlan,
Bradley Schmerl and
Jichuan Chang. Using Gauges for Architecture-Based Monitoring and Adaptation. In Proceedings of the Working Conference on Complex and Dynamic Systems Architecture. December 12-14, 2001.
Abstract: An increasingly important requirement for complex systems is the capability to adapt at runtime in order to accommodate variable resources, system errors, and changing requirements. An essential aspect of adaptation is the ability to observe a system's runtime behavior and interpret those observations in terms that permit a high-level understanding of the system's status. In this paper we describe mechanisms for monitoring a running system, interpreting monitored data in terms of the system's architecture, and analyzing the system architecture to ascertain if the system's runtime behavior fits within the envelope of acceptable behavior. We illustrate the use of these mechanisms for the important special case of system performance monitoring.