In self-adaptive software systems, the role of context is paramount, especially for proactive self-adaptation. Current research, however, does not fully explore context's impact, for example on priorities of the requirements. To address this gap, we introduce a novel contextual goal model to capture these factors and their influence on the system. Using this, we propose a two-layer control mechanism with a context-aware model predictive control to achieve proactive adaptation for the software system and adaptation for the controller itself. By contextual prediction and a more accurate system model, our approach utilizes model predictive control to facilitate timely and efficient system adaptations, improving both performance and adaptability. Meanwhile, we perform requirement adaptation to update the contextual goal model, which in turn updates the objective function and constraints of the controller. Our experimental evaluations across two scenarios demonstrate the significant benefits of our approach in enhancing system performance.

Algorithmic fairness of machine learning (ML) models has raised significant concern in the recent years. Many testing, verification, and bias mitigation techniques have been proposed to identify and reduce fairness issues in ML models. The existing methods are model-centric and designed to detect fairness issues under static settings. However, many ML-enabled systems operate in a dynamic environment where the predictive decisions made by the system impact the environment, which in turn affects future decision-making. Such a self-reinforcing feedback loop can cause fairness violations in the long term, even if the immediate outcomes are fair. In this paper, we propose a simulation-based framework called Fairsenseto detect and analyze long-term unfairness in ML-enabled systems. Given a fairness requirement, Fairsenseperforms Monte-Carlo simulation to enumerate evolution traces for each system configuration. Then, Fairsenseperforms sensitivity analysis on the space of possible configurations to understand the impact of design options and environmental factors on the long-term fairness of the system. We demonstrate Fairsense'spotential utility through three real-world case studies: Loan lending, opioids risk scoring, and predictive policing.

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.

Ensuring safety and providing rigorous behavioral guarantees are critical for robotic systems operating in high-stakes environments such as autonomous driving. Field testing is common, but costly and risky. Simulation-based testing offers a safer and lower-cost alternative for automatically generating traces for analysis and performance assessment. An oracle is essential for evaluating each trace, assessing whether a robot behavior fulfills key criteria such as task completion, safety, efficiency, and reliability. Supervised learning for oracle learning is accurate but costly and time-consuming due to manual labeling, whereas unsupervised learning requires no labels but often sacrifices accuracy. To overcome these limitations, we propose human-in-the-loop oracle learning as a new approach to develop and refine oracles that are capable of distinguishing good from bad behaviors with reduced manual effort. We illustrate this approach through a conceptual framework for integrating human-in-the-loop learning into robotic system evaluation.

Human error is often associated with system failures. The complexity of human-automation interaction can make it difficult to anticipate what errors can occur and how they contribute to failures. Previous research has shown that task analytic behavior modeling with the enhanced operator function model and the cognitive reliability analysis method (CREAM) can be combined with statistical model checking to make predictions about human error rates, their stochastic impact on system failures, and the effect of negative transfer of design changes on these predictions. These efforts were successful, but the validation studies used artificial examples with limited data. Predictions also slightly overestimated error rates. This article addresses these deficiencies by conducting a validation study based on the prescription order entry interface of the OpenEMR electronic medical record. As part of this, we explored how prediction accuracy for the OpenEMR application changed based on the inclusion/exclusion of planning errors: errors based on people’s ability to formulate task plans, which we hypothesized contributed to error rate overestimation. Results found that our method’s predictions aligned with those observed in the experiment, especially when planning errors were excluded. Negative transfer conditions did not manifest significant differences in error rates experimentally or in model predictions. These results suggest that negative transfer’s impact on human–computer interaction may be overstated in the literature. Finally, higher error rates were observed between the original OpenEMR prescription order entry interface compared to an alternative that we tested. We highly suggest that OpenEMR adopt the alternative.

Abstract Cyber-physical systems (CPS) with reinforcement learning (RL)-based controllers are increasingly being deployed in complex physical 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 uncertainties in the actual operation. In this paper, we introduce a new, expressive notion of tolerance that describes how well a controller is capable 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 tolerance 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 construct 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.

Social media provide a steady diet of dire warnings that artificial intelligence (AI) will make software engineering (SE) irrelevant or obsolete. To the contrary, the engineering discipline of software is rich and robust; it encompasses the full scope of software design, development, deployment, and practical use; and it has regularly assimilated radical new offerings from AI. Current AI innovations such as machine learning, large language models (LLMs) and generative AI will offer new opportunities to extend the models and methods of SE. They may automate some routine development processes, and they will bring new kinds of components and architectures. If we're fortunate they may force SE to rethink what we mean by correctness and reliability. They will not, however, render SE irrelevant.

Security attacks present unique challenges to the design of self-adaptation mechanism for software-intensive systems due to the adversarial nature of the environment. Game-theoretical approaches have been explored in security to model malicious behaviors and design reliable defense for the system in a mathematically grounded manner. However, modeling the system as a single player, as done in prior works, is insufficient for the system under partial compromise and for the design of fine-grained defensive policies where the rest of the system with autonomy can cooperate to mitigate the impact of attacks. To address such issues, we propose a new self-adaptation framework incorporating Bayesian game theory and model the defender (i.e., the system) at the granularity of components. Under security attacks, the architecture model of the system is automatically translated, by the proposed translation process with designed algorithms, into a multi-player Bayesian game. This representation allows each component to be modeled as an independent player, while security attacks are encoded as variant types for the components. By solving for pure equilibrium (i.e., adaptation response), the system’s optimal defensive strategy is dynamically computed, enhancing system resilience against security attacks by maximizing system utility. We validate the effectiveness of our framework through two sets of experiments using generic benchmark tasks tailored for the security domain. Additionally, we exemplify the practical application of our approach through a real-world implementation in the Secure Water Treatment System to demonstrate the applicability and potency in mitigating security risks.

Abstract A safety verification task involves verifying a system against a desired safety property under certain assumptions about the environment. However, these environmental assumptions may occasionally be violated due to modeling errors or faults. Ideally, the system guarantees its critical properties even under some of these violations, i.e., the system is robust against environmental deviations. This paper proposes a notion of robustness as an explicit, first-class property of a transition system that captures how robust it is against possible deviations in the environment. We modeled deviations as a set of transitions that may be added to the original environment. Our robustness notion then describes the safety envelope of this system, i.e., it captures all sets of extra environment transitions for which the system still guarantees a desired property. We show that being able to explicitly reason about robustness enables new types of system analysis and design tasks beyond the common verification problem stated above. We demonstrate the application of our framework on case studies involving a radiation therapy interface, an electronic voting machine, a fare collection protocol, and a medical pump device.

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.

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

Decision making in self-adaptive systems often involves trade-offs between multiple quality attributes, with user preferences that indicate the relative importance and priorities among the attributes. However, eliciting such preferences accurately from users is a difficult task, as they may find it challenging to specify their preference in a precise, mathematical form. Instead, they may have an easier time expressing their displeasure when the system does not exhibit behaviors that satisfy their internal preferences. Furthermore, the user’s preference may change over time depending on the environmental context; thus, the system may be required to continuously adapt its behavior to satisfy this change in preference. However, existing self-adaptive frameworks do not explicitly consider dynamic human preference as one of the sources of uncertainty. In this paper, we propose a new adaptation framework that is specifically designed to support self-adaptation to user preference. Our framework takes a human-on-the-loop approach where the user is given an ability to intervene and indicate dissatisfaction and corrections with the current behavior of the system; in such a scenario, the system automatically updates the existing preference values so that the new, resulting behavior of the system is consistent with the user’s notion of satisfactory behavior. To perform this adaptation, we propose a novel similarity analysis to produce changes in the preference that are optimal with respect to the system utility. We illustrate our approach in a case study involving a delivery robot system. Our preliminary results indicate that our approach can effectively adapt its behavior to changing human preference.

Previous research has shown how statistical model checking can be used with human task behavior modeling and human reliability analysis to make realistic predictions about human errors and error rates. However, these efforts have not accounted for the impact that design changes can have on human reliability. In this research, we address this deficiency by using similarity theory from human cognitive modeling. This replicates how negative transfer can cause people to perform old task behaviors on modified systems. We present details about how this approach was realized with the PRISM model checker and the enhanced operator function model. We report results of a validation exercise using an application from the literature. We discuss the implications of our results and describe future research.

A weakly-hard fault model can be captured by an (m,k) constraint, where 0≤ m ≤ k , meaning that there are at most m bad events (faults) among any k consecutive events. In this article, we use a weakly-hard fault model to constrain the occurrences of faults in system inputs. We develop approaches to verify properties for all possible values of (m,k) , where k is smaller than or equal to a given K , in an exact and efficient manner. By verifying all possible values of (m,k) , we define weakly-hard requirements for the system environment and design a runtime monitor based on counting the number of faults in system inputs. If the system environment satisfies the weakly-hard requirements, then the satisfaction of desired properties is guaranteed; otherwise, the runtime monitor can notify the system to switch to a safe mode. This is especially essential for cyber-physical systems that need to provide guarantees with limited resources and the existence of faults. Experimental results with discrete second-order control, network routing, vehicle following, and lane changing demonstrate the generality and the efficiency of the proposed approaches.

In system design, high-level system models typically need to be mapped to an execution platform (e.g., hardware, environment, compiler, etc). The platform may naturally strengthen some constraints or weaken some others, but it is expected that the low-level implementation on the platform should preserve all the functional and extra-functional properties of the model, including the ones for information-flow security. It is, however, well known that simple notions of refinement do not preserve information-flow security properties. In this paper, we propose a novel automated mapping synthesis approach that preserves hyperproperties expressed in the temporal logic HyperLTL. The significance of our technique is that it can handle formulas with quantifier alternations, which is typically the source of difficulty in refinement for information-flow security policies. We reduce the mapping synthesis problem to HyperLTL model checking and leverage recent efforts in bounded model checking for hyperproperties. We demonstrate how mapping synthesis can be used in various applications, including enforcing non-interference and automating secrecy-preserving refinement mapping. We also evaluate our approach using the battleship game and password validation use cases.

Many self-adaptive systems benefit from human involvement and oversight, where a human operator can provide expertise not available to the system and detect problems that the system is unaware of. One way of achieving this synergy is by placing the human operator on the loop —i.e., providing supervisory oversight and intervening in the case of questionable adaptation decisions. To make such interaction effective, an explanation can play an important role in allowing the human operator to understand why the system is making certain decisions and improve the level of knowledge that the operator has about the system. This, in turn, may improve the operator’s capability to intervene and, if necessary, override the decisions being made by the system. However, explanations may incur costs, in terms of delay in actions and the possibility that a human may make a bad judgment. Hence, it is not always obvious whether an explanation will improve overall utility and, if so, then what kind of explanation should be provided to the operator. In this work, we define a formal framework for reasoning about explanations of adaptive system behaviors and the conditions under which they are warranted. Specifically, we characterize explanations in terms of explanation content , effect , and cost . We then present a dynamic system adaptation approach that leverages a probabilistic reasoning technique to determine when an explanation should be used to improve overall system utility. We evaluate our explanation framework in the context of a realistic industrial control system with adaptive behaviors.

Abstract Security attacks present unique challenges to self-adaptive system design due to the adversarial nature of the environment. Game theory approaches have been explored in security to model malicious behaviors and design reliable defense for the system in a mathematically grounded manner. However, modeling the system as a single player, as done in prior works, is insufficient for the system under partial compromise and for the design of fine-grained defensive strategies where the rest of the system with autonomy can cooperate to mitigate the impact of attacks. To deal with such issues, we propose a new self-adaptive framework incorporating Bayesian game theory and model the defender (i.e., the system) at the granularity ofcomponents. Under security attacks, the architecture model of the system is translated into aBayesian multi-player game, where each component is explicitly modeled as an independent player while security attacks are encoded as variant types for the components. The optimal defensive strategy for the system is dynamically computed by solving the pure equilibrium (i.e., adaptation response) to achieve the best possible system utility, improving the resiliency of the system against security attacks. We illustrate our approach using an example involving load balancing and a case study on inter-domain routing.

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.

The feature interaction problem arises when two or more independent features interact with each other in an undesirable manner. Feature interactions remain a challenging and important problem in emerging domains of cyber-physical systems (CPS), such as intelligent vehicles, unmanned aerial vehicles (UAVs) and the Internet of Things (IoT), where the outcome of an unexpected interaction may result in a safety failure. Existing approaches to resolving feature interactions rely on priority lists or fixed strategies, but may not be effective in scenarios where none of the competing feature actions are satisfactory with respect to system requirements. This paper proposes a novel synthesis-based approach to resolution, where a conflict among features is resolved by synthesizing an action that best satisfies the specification of desirable system behaviors in the given environmental context. Unlike existing resolution methods, our approach is capable of producing a desirable system outcome even when none of the conflicting actions are satisfactory. The effectiveness of the proposed approach is demonstrated using a case study involving interactions among safety-critical features in an autonomous drone.

In this paper, we propose a robust solution for the path planning and scheduling of the moving objects in a Track-based Traffic Control System (TTCS). The moving objects in a TTCS pass over pre-specified sub-tracks. Each sub-track accommodates at most one moving object in-transit. Due to the uncertainties in the context of a TTCS, we assign an arrival time window to each moving object for each sub-track in its route, instead of an exact value. The moving object can safely enter into the sub-track in the mentioned time window. To develop a safe plan, we adapt the tagged-signal model and provide a rigorous mathematical formalism for the actor model of a TTCS. To illustrate the applicability of the provided semantics, we provide a formal model of TTCSs in the Alloy language and use its analyzer to verify the developed model against system safety properties.

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 defined 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.

An emerging type of network architecture called edge computing has the potential to improve the availability and resilience of IoT services under anomalous situations such as network failures or denial-of-service (DoS) attacks. However, relatively little has been explored on the problem of ensuring availability even when edge computers that provide key security services (e.g., authentication and authorization) become unavailable themselves. This article proposes a resilient authentication and authorization framework to enhance the availability of IoT services under DoS attacks or failures. The proposed approach leverages a technique called secure migration , which allows an IoT device to migrate to another trusted edge computer when its own local authorization service becomes unavailable. Specifically, we describe the design of a secure migration framework and its supporting mechanisms, including (1) automated migration policy construction and (2) protocols for preparing and executing the secure migration. We formalize secure migration policy construction as an integer linear programming (ILP) problem and show its effectiveness using a case study on smart buildings, where the proposed solution achieves significantly higher availability under simulated attacks on authorization services.

In this paper, we propose a game theoretical adversarial intervention detection mechanism for reliable smart road signs. A future trend in intelligent transportation systems is “smart road signs” that incorporate smart codes (e.g., visible at infrared) on their surface to provide more detailed information to smart vehicles. Such smart codes make road sign classification problem aligned with communication settings more than conventional classification. This enables us to integrate well-established results in communication theory, e.g., error-correction methods, into road sign classification problem. Recently, vision-based road sign classification algorithms have been shown to be vulnerable against (even) small scale adversarial interventions that are imperceptible for humans. On the other hand, smart codes constructed via error-correction methods can lead to robustness against small scale intelligent or random perturbations on them. In the recognition of smart road signs, however, humans are out of the loop since they cannot see or interpret them. Therefore, there is no equivalent concept of imperceptible perturbations in order to achieve a comparable performance with humans. Robustness against small scale perturbations would not be sufficient since the attacker can attack more aggressively without such a constraint. Under a game theoretical solution concept, we seek to ensure certain measure of guarantees against even the worst case (intelligent) attackers that can perturb the signal even at large scale. We provide a randomized detection strategy based on the distance between the decoder output and the received input, i.e., error rate. Finally, we examine the performance of the proposed scheme over various scenarios.

System development often involves decisions about how a high-level design is to be implemented using primitives from a low-level platform. Certain decisions, however, may introduce undesirable behavior into the resulting implementation, possibly leading to a violation of a desired property that has already been established at the design level. In this paper, we introduce the problem of synthesizing a property-preserving platform mapping: synthesize a set of implementation decisions ensuring that a desired property is preserved from a high-level design into a low-level platform implementation. We formalize this synthesis problem and propose a technique for generating a mapping based on symbolic constraint search. We describe our prototype implementation, and two real-world case studies demonstrating the applicability of our technique to the synthesis of secure mappings for the popular web authorization protocols OAuth 1.0 and 2.0.

Assume-guarantee (A/G) contracts are mathematical models enabling modular and hierarchical design and verifi-cation of complex systems by rigorous decomposition of system-level specifications into component-level specifications. Existing A/G contract frameworks, however, are not designed to effectively capture the behaviors of cyber-physical systems where multiple agents aim to maximize one or more objectives, and may interact with each other and the environment in a cooperative or non-cooperative way toward achieving their goals. We propose an extension of the A/G contract framework, namely optimizing A/G contracts, that can be used to specify and reason about properties of component interactions that involve optimizing objectives. The proposed framework includes methods for constructing new contracts via conjunction and composition, along with algorithms to verify system properties via contract refinement. We illustrate its effectiveness on a set of case studies from connected and autonomous vehicles.

Emerging applications in connected vehicles have tremendous potential for advances in safety, navigation, traffic management and fuel efficiency, while also posing new security challenges such as false information attacks. This paper targets the problem of securing critical information that is disseminated among nearby vehicles for safety and traffic efficiency purposes through distributed consensus. We present a consensus algorithm, which uses a "proof of eligibility" test to establish that a group of vehicles are actually within the vicinity of the information source. With the presence of a limited number of compromised (Byzantine faulty) participants, our algorithm provides correct consensus among healthy vehicles in real time. The algorithm provides fast and reliable consensus group formation and private key distribution without privileged members, trusted setup, or leader election. In addition to proving a safety property of our consensus algorithm, we have implemented it on top of a widely-used vehicle simulation environment (SUMO, OMNeT++ and Veins) and evaluated its performance on a model of the streets in a real midtown area. Simulation results demonstrate that the algorithm can reach consensus very efficiently (within 9.5s) and with up to 30% of compromised vehicles in a given area. The simulations also demonstrate the ability of our algorithm to more quickly disseminate information about a traffic accident and more efficiently route traffic around the accident site, as compared to previous robust information dissemination approaches.

Advanced driver-assistance systems (ADAS), autonomous driving, and connectivity have enabled a range of new features, but also made automotive design more complex than ever. Formal verification can be applied to establish functional correctness, but its scalability is limited due to the sheer complexity of a modern automotive system. To manage high complexity and limited development resources, one alternative is to apply runtime monitoring techniques to detect when the system transitions into an unsafe state (i.e., one where it violates a critical safety requirement). In this paper, we report on our experience integrating runtime monitoring into a development workflow and present practical design considerations on languages and tools from an industrial perspective. Using signal temporal logic (STL) [12] and the Breach [6] monitoring tool, we perform a case study showing how monitoring can be used to detect undesirable interactions between two ADAS features called Cooperative Pile-up Mitigation System (CPMS) and False-Start Prevention System (FPS). This is an initial step to utilize runtime monitoring to achieve high assurance in the design of intelligent vehicles.

Connected vehicle applications such as autonomous intersections and intelligent traffic signals have shown great promises in improving transportation safety and efficiency. However, security is a major concern in these systems, as vehicles and surrounding infrastructures communicate through ad-hoc networks. In this paper, we will first review security vulnerabilities in connected vehicle applications. We will then introduce and discuss some of the defense mechanisms at network and system levels, including (1) the Security Credential Management System (SCMS) proposed by the United States Department of Transportation, (2) an intrusion detection system (IDS) that we are developing and its application on collaborative adaptive cruise control, and (3) a partial consensus mechanism and its application on lane merging. These mechanisms can assist to improve the security of connected vehicle applications.

We introduce a novel notion of quotient set for a pair of contracts and the operation of quotient for assume-guarantee contracts. The quotient set and its related operation can be used in any compositional methodology where design requirements are mapped into a set of components in a library. In particular, they can be used for the so called missing component problem, where the given components are not capable of discharging the obligations of the requirements. In this case, the quotient operation identifies the contract for a component that, if added to the original set, makes the resulting system fulfill the requirements.

Driving is a social activity which involves endless interactions with other agents on the road. Failing to locate these agents and predict their possible future actions may result in serious safety hazards. Traditionally, the responsibility for avoiding these safety hazards is solely on the drivers. With improved sensor quantity and quality, modern ADAS systems are able to accurately perceive the location and speed of other nearby vehicles and warn the driver about potential safety hazards. However, accurately predicting the behavior of a driver remains a challenging problem. In this paper, we propose a framework in which behavioral models of drivers (Digital Behavioral Twins) are shared among connected cars to predict potential future actions of neighboring vehicles, therefore improving the safety of driving. We provide mathematical formulations of models of driver behavior and the environment, and discuss challenging problems during model construction and risk analysis. We also demonstrate that our digital twins framework can accurately predict driver behaviors and effectively prevent collisions using a case study in a virtual driving simulation environment.

Abstract The ever increasing expansion of mobile applications into nearly every aspect of modern life, from banking to healthcare systems, is making their security more important than ever. Modern smartphone operating systems (OS) rely substantially on the permission-based security model to enforce restrictions on the operations that each application can perform. In this paper, we perform an analysis of the permission protocol implemented in Android, a popular OS for smartphones. We propose a formal model of the Android permission protocol in Alloy, and describe a fully automatic analysis that identifies potential flaws in the protocol. A study of real-world Android applications corroborates our finding that the flaws in the Android permission protocol can have severe security implications, in some cases allowing the attacker to bypass the permission checks entirely.

Normative systems (i.e., a set of rules) are an important approach to achieving effective coordination among (often an arbitrary number of) agents in multiagent systems. A normative system should be effective in ensuring the satisfaction of a desirable system property, and minimal (i.e., not containing norms that unnecessarily over-constrain the behaviors of agents). Designing or even automatically synthesizing minimal effective normative systems is highly non-trivial. Previous attempts on synthesizing such systems through simulations often fail to generate normative systems which are both minimal and effective. In this work, we propose a framework that facilitates designing of minimal effective normative systems using lightweight formal methods. Given a minimal effective normative system which coordinates many agents must be minimal and effective for a small number of agents, we start with automatically synthesizing one such system with a few agents. We then increase the number of agents so as to check whether the same design remains minimal and effective. If it is, we manually establish an induction proof so as to lift the design to an arbitrary number of agents.

Security attacks often exploit flaws that are not anticipated in an abstract design, but are introduced inadvertently when high-level interactions in the design are mapped to low-level behaviors in the supporting platform. This paper proposes a multi-representational approach to security analysis, where models capturing distinct (but possibly overlapping) views of a system are automatically composed in order to enable an end-to-end analysis. This approach allows the designer to incrementally explore the impact of design decisions on security, and discover attacks that span multiple layers of the system. This paper describes Poirot, a prototype implementation of the approach, and reports on our experience on applying Poirot to detect previously unknown security flaws in publicly deployed systems.

The last decade has seen a dramatic growth in the use of constraint solvers as a computational mechanism, not only for analysis of software, but also at runtime. Solvers are available for a variety of logics but are generally restricted to first-order formulas. Some tasks, however, most notably those involving synthesis, are inherently higher order; these are typically handled by embedding a first-order solver (such as a SAT or SMT solver) in a domain-specific algorithm. Using strategies similar to those used in such algorithms, we show how to extend a first-order solver (in this case Kodkod, a model finder for relational logic used as the engine of the Alloy Analyzer) so that it can handle quantifications over higher-order structures. The resulting solver is sufficiently general that it can be applied to a range of problems; it is higher order, so that it can be applied directly, without embedding in another algorithm; and it performs well enough to be competitive with specialized tools. Just as the identification of first-order solvers as reusable backends advanced the performance of specialized tools and simplified their architecture, factoring out higher-order solvers may bring similar benefits to a new class of tools.

A dependability case is an explicit, end-to-end argument, based on concrete evidence, that a system satisfies a critical property. We report on a case study constructing a dependability case for the control software of a medical device. The key novelty of our approach is a lightweight code analysis that generates a list of side conditions that correspond to assumptions to be discharged about the code and the environment in which it executes. This represents an unconventional trade-off between, at one extreme, more ambitious analyses that attempt to discharge all conditions automatically (but which cannot even in principle handle environmental assumptions), and at the other, flow- or context-insensitive analyses that require more user involvement. The results of the analysis suggested a variety of ways in which the dependability of the system might be improved.

Model-driven architecture (MDA) is a model-based approach for engineering complex software systems. MDA is particularly attractive for designing embedded systems because models can be easily evolved as hardware and software requirements evolve. However, efforts to apply MDA in industrial settings expose several open problems surrounding tooling: Engineers need automated techniques that are scalable, general, and extensible. In this paper we describe the formula framework as a novel approach towards general automation for MDA. We develop a running example and benchmarks to compare our tools with other state-of-theart approaches.

We propose a set of patterns for structuring a system to be dependable by design. The key idea is to localize the system's most critical requirements into small, reliable parts called trusted bases. We describe two instances of trusted bases: (1) the end-to-end check, which localizes the correctness checking of a computation to end points of a system, and (2) the trusted kernel, which ensures the safety of a set of resources with a small core of a system.

An approach is suggested for arguing that a system is dependable. The key idea is to structure the system so that critical requirements are localized in small, reliable subsets of the system's components called trusted bases. This paper describes an idiom for modeling systems with trusted bases, and a technique for analyzing a dependability argument-the argument that a trusted base is sufficient to establish a requirement.