Biblio

Self-adaptive systems overcome many of the limitations of human supervision in complex software-intensive systems by endowing them with the ability to automatically adapt their structure and behavior in the presence of runtime changes. However, adaptation in some classes of systems (e.g., safetycritical) can benefit by receiving information from humans (e.g., acting as sophisticated sensors, decision-makers), or by involving them as system-level effectors to execute adaptations (e.g., when automation is not possible, or as a fallback mechanism). However, human participants are influenced by factors external to the system (e.g., training level, fatigue) that affect the likelihood of success when they perform a task, its duration, or even if they are willing to perform it in the first place. Without careful consideration of these factors, it is unclear how to decide when to involve humans in adaptation, and in which way. In this paper, we investigate how the explicit modeling of human participants can provide a better insight into the trade-offs of involving humans in adaptation. We contribute a formal framework to reason about human involvement in self-adaptation, focusing on the role of human participants as actors (i.e., effectors) during the execution stage of adaptation. The approach consists of: (i) a language to express adaptation models that capture factors affecting human behavior and its interactions with the system, and (ii) a formalization of these adaptation models as stochastic multiplayer games (SMGs) that can be used to analyze humansystem-environment interactions. We illustrate our approach in an adaptive industrial middleware used to monitor and manage sensor networks in renewable energy production plants.

In this work we develop a novel Bayesian neural network methodology to achieve strong adversarial robustness without the need for online adversarial training. Unlike previous efforts in this direction, we do not rely solely on the stochasticity of network weights by minimizing the divergence between the learned parameter distribution and a prior. Instead, we additionally require that the model maintain some expected uncertainty with respect to all input covariates. We demonstrate that by encouraging the network to distribute evenly across inputs, the network becomes less susceptible to localized, brittle features which imparts a natural robustness to targeted perturbations. We show empirical robustness on several benchmark datasets.

End-users’ trust in automated agents is important as automated decision-making and planning is increasingly used in many aspects of people’s lives. In real-world applications of planning, multiple optimization objectives are often involved. Thus, planning agents’ decisions can involve complex tradeoffs among competing objectives. It can be difficult for the end-users to understand why an agent decides on a particular planning solution on the basis of its objective values. As a result, the users may not know whether the agent is making the right decisions, and may lack trust in it. In this work, we contribute an approach, based on contrastive explanation, that enables a multi-objective MDP planning agent to explain its decisions in a way that communicates its tradeoff rationale in terms of the domain-level concepts. We conduct a human subjects experiment to evaluate the effectiveness of our explanation approach in a mobile robot navigation domain. The results show that our approach significantly improves the users’ understanding, and confidence in their understanding, of the tradeoff rationale of the planning agent.

Programming languages exist to enable people to create and maintain software as effectively as possible. They are subject to two very different sets of requirements: first, the need to provide strong safety guarantees to protect against bugs; and second, the need for users to effectively and efficiently write software that meets their functional and quality requirements. This thesis argues that fusing formal methods for reasoning about programming languages with user-centered design methods is a practical approach to designing languages that make programmers more effective. By doing so, designers can create safer languages that are more effective for programmers than existing languages. The thesis is substantiated by the introduction of PLIERS: Programming Language Iterative Evaluation and Refinement System. PLIERS is a process for designing programming languages that integrates formal methods with user-centered design. The hypothesis that PLIERS is beneficial is supported by two language design projects. In these projects, I show how PLIERS benefits the programming language design process. Glacier is an extension to Java that enforces transitive class immutability, which is a much stronger property than that provided by languages that are in use today. Although there are hundreds of possible ways of restricting changes to state in programming languages, Glacier occupies a point in the design space that was justified by interview studies with professional software engineers. I evaluated Glacier in case studies, showing that it is expressive enough for some real-world applications. I also evaluated Glacier in lab studies and compared it to Java’s final keyword, finding both that Glacier is more effective at expressing immutability than final and that Glacier detects bugs that users are likely to insert in code. Blockchains are a distributed computing platform that aim to enable safe computation among users who do not necessarily trust each other. To improve safety relative to existing languages, in which programmers have repeatedly deployed software with serious bugs, I designed Obsidian, a new programming language for blockchain application development. From observations about typical blockchain applications, I derived two features that motivated the design of Obsidian. First, blockchain applications typically implement state machines, which support different operations in different states. Obsidian uses typestate, which lifts dynamic state into static types, to provide static guarantees regarding object state. Second, blockchain applications frequently manipulate resources, such as virtual currency. Obsidian provides a notion of ownership, which distinguishes one reference from all others. Obsidian supports resources via linear types, which ensure that owning references to resources are not accidentally lost. The combination of resources and typestate results in a novel set of design problems for the type system; although each idea has been explored individually, combining them requires unifying different perspectives on linearity. Furthermore, no language with either one of these features has been designed in a user-centered way or evaluated with users. Typical typestate systems have a complex set of permissions that provides safety properties, but these systems focused on expressiveness rather than on usability. Obsidian integrates typestate and resources in a novel way, resulting in a new type system design with a focus on simplicity and usability while retaining the desired safety properties. Obsidian is based on a core calculus I designed, Silica, for which I proved type soundness. In order to make Obsidian as usable as possible, I based its design on the results of formative studies with programmers. I evaluated Obsidian with two case studies, showing that Obsidian can be used to implement relevant programs. I also conducted a randomized controlled trial comparing Obsidian to Solidity, a popular language for writing smart contracts. I found that most of the Obsidian participants learned Obsidian and completed programming tasks after only a short training period; further, in one task, 70% of the participants who used Solidity accidentally inserted bugs that Obsidian’s compiler would have detected. Finally, Obsidian participants completed significantly more tasks correctly than did Solidity participants.

Blockchains host smart contracts for voting, tokens, and other purposes. Vulnerabilities in contracts are common, often leading to the loss of money. Psamathe is a new language we are designing around a new flow abstraction, reducing asset bugs and making contracts more concise than in existing languages. We present an overview of Psamathe, and discuss two example contracts in Psamathe and Solidity.

Realistic state-based discrete-event simulation models are often quite complex. The complexity frequently manifests in models that (a) contain a large number of input variables whose values are difficult to determine precisely, and (b) take a relatively long time to solve. Traditionally, models that have a large number of input variables whose values are not well-known are understood through the use of sensitivity analysis (SA) and uncertainty quantification (UQ). However, it can be prohibitively time consuming to perform SA and UQ. In this work, we present a novel approach we developed for performing fast and thorough SA and UQ on a metamodel composed of a stacked ensemble of regressors that emulates the behavior of the base model. We demonstrate the approach using a previously published botnet model as a test case, showing that the metamodel approach is several orders of magnitude faster than the base model, more accurate than existing approaches, and amenable to SA and UQ.