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: 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: Advanced persistent threats (APTs) are a particularly troubling challenge
for software systems. The adversarial nature of the security
domain, and APTs in particular, poses unresolved challenges to
the design of self- systems, such as how to defend against multiple
types of attackers with different goals and capabilities. In
this interaction, the observability of each side is an important and
under-investigated issue in the self- domain. We propose a model
of APT defense that elevates observability as a first-class concern.
We evaluate this model by showing how an informed approach that
uses observability improves the defender’s utility compared to a
uniform random strategy, can enable robust planning through sensitivity
analysis, and can inform observability-related architectural
design decisions.
Abstract: Modern cyber-physical systems (e.g., robotics systems) are typically composed of physical and software components, the characteristics of which are likely to change over time.
Assumptions about parts of the system made at design time may not hold at run time, especially when a system is deployed for long periods (e.g., over decades).
Self-adaptation is designed to find reconfigurations of systems to handle such run-time inconsistencies. Planners can be used to find and enact optimal reconfigurations in such an evolving context. However, for systems that are highly configurable, such planning becomes intractable due to the size of the adaptation space.
To overcome this challenge, in this paper we explore an approach that (a) uses machine learning to find Pareto-optimal configurations without needing to explore every configuration, and (b) restricts the search space to such configurations to make planning tractable.
We explore this in the context of robot missions that need to consider task timeliness and energy consumption. An independent evaluation shows that our approach results in high quality adaptation plans in uncertain and adversarial environments.
Abstract: This paper presents a framework for engineering resource-adaptive software systems targeted at small
mobile devices. The proposed framework empowers users to control tradeoffs among a rich set of servicespecific
aspects of quality of service. After motivating the problem, the paper proposes a model for
capturing user preferences with respect to quality of service, and illustrates prototype user interfaces to elicit
such models. The paper then describes the extensions and integration work made to accommodate the
proposed framework on top of an existing software infrastructure for ubiquitous computing.
The research question addressed here is the feasibility of coordinating resource allocation and
adaptation policies in a way that end-users can understand and control in real time. The evaluation covered
both systems and the usability perspectives, the latter by means of a user study. The contributions of this
work are: first, a set of design guidelines for resource-adaptive systems, including APIs for integrating new
applications; second, a concrete infrastructure that implements the guidelines. And third, a way to model
quality of service tradeoffs based on utility theory, which our research indicates end-users with diverse
backgrounds are able to leverage for guiding the adaptive behaviors towards activity-specific quality goals.
Abstract: Self-adapting systems based on multiple concurrent applications must decide how to allocate scarce resources to
applications and how to set the quality parameters of each
application to best satisfy the user. Past work has made
those decisions with analytic models that used current resource availability information: they react to recent changes in resource availability as they occur, rather than anticipating future availability. These reactive techniques may model each local decision optimally, but the accumulation of decisions over time nearly always becomes less than optimal.
In this paper, we propose an approach to self adaptation, called anticipatory configuration that leverages
predictions of future resource availability to improve utility for the user over the duration of the task. The approach solves the following technical challenges: (1) how to express resource availability prediction, (2) how to combine prediction from multiple sources, and (3) how to leverage predictions continuously while improving utility to the user. Our experiments show that when certain adaptation operations are costly, anticipatory configuration provides better utility to the user than reactive configuration, while being comparable in resource demand.
Abstract: One of the challenges for software architects is ensuring that an implemented system faithfully represents its architecture. We describe and demonstrate a tool, called DiscoTect, that addresses this challenge by dynamically monitoring a running system and deriving the software architecture as that system runs. The derivation process is based on mappings that relate low level system-level events to higher-level architectural events. The resulting architecture is then fed into existing architectural design tools so that comparisons can be conducted with the design time architecture and architectural analyses can be re-run to ensure that they are still valid. In addition to the demonstration, we briefly describe the mapping language and formal definition of the language in terms of Colored Petri Nets.
Abstract: One of the challenging problems for software developers is guaranteeing that a system as built is consistent with its architectural design. In this paper we describe a technique that uses run time observations about an executing system to construct an architectural view of the system. With this technique we develop mappings that exploit regularities in system implementation and architectural style. These mappings describe how low-level system events can be interpreted as more abstract architectural operations. We describe the current implementation of a tool that uses these mappings, and show that it can highlight inconsistencies between implementation and architecture.