Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Synthesis of Robust Control Software

PIs: Tabuada (UCLA)

According to the IEEE standard glossary of software engineering, robustness is the degree to which a system or component can function correctly in the presence of invalid inputs or stressful environment conditions. Our contribution is a synthesis methodology for robust cyber-physical systems (CPS) based on a notion of robustness for CPS termed inputoutput dynamical stability [RT13,RT14a,RT14b,TCRM14]. It captures two intuitive aims of a robust design: bounded disturbances have bounded consequences and the effect of sporadic disturbances disappears as time progresses. Our synthesis framework is based on an abstraction and refinement procedure. We first compute a finite-state abstraction for the physical components that can be used to synthesize a reactive controller enforcing robustness with respect to discrete environments. This preliminary design is then refined to the reactive control software interacting with the physical components. The refinement step is based on control theoretic techniques so as to provide robustness with respect to continuous environments. The resulting design is then robust with respect to both discrete and continuous environments. In order to establish the preservation of robustness through the abstraction and refinement process we developed several new notions of simulation and bisimulation. Future work includes an experimental validation of these ideas in the context of the robotic systems challenge problem.We have already made preliminary steps towards this objective by investigating reactive control software synthesis for robotic systems in collaboration with Kress-Gazit’s group.


Optimal Performance for Continuous-time Controllers

PI: Kress-Gazit (Cornell)

Recently, formal methods have been used to transform high-level robot tasks into correct-by-construction controllers. While correctness is guaranteed, these inherently discrete methods can often lead to behaviors that are not optimal in the continuous sense, i.e. they induce robot paths that are significantly suboptimal. This work proposes an algorithm for dynamically reordering the robot goals and connecting them with the shortest path based on the given continuous metric. The generated robot trajectories are close-to-optimal while satisfying the original task specification in a dynamic environment. This method is implemented and simulation results are shown. The results are being integrated in the tool LTLMoP to be applied to the Robotics challenge problem [WFK13].


Synthesis of Controllers for Linear Systems

PI: Tabuada (UCLA)

In this work, we present and analyze a novel algorithm to synthesize controllers enforcing linear temporal logic specifications on discrete-time linear systems. The central step within this approach is the computation of the maximal controlled invariant set contained in a possibly non-convex safe set. Although it is known how to compute approximations of maximal controlled invariant sets, its exact computation remains an open problem. We provide an algorithm which computes a controlled invariant set that is guaranteed to be an under-approximation of the maximal controlled invariant set. Moreover, we guarantee that our approximation is at least as good as any invariant set whose distance to the boundary of the safe set is lower bounded. The proposed algorithm is founded on the notion of sets adapted to the dynamics and binary decision diagrams. Contrary to most controller synthesis schemes enforcing temporal logic specifications on continuous systems, we do not compute a discrete abstraction of the continuous dynamics. Instead, we abstract only the part of the continuous dynamics that is relevant for the computation of the maximal controlled invariant set. For this reason we call our approach specification guided. We describe the theoretical foundations and technical underpinnings of a preliminary implementation and report on several experiments including the synthesis of an automatic cruise controller. Our preliminary implementation handles up to five continuous dimensions and specifications containing up to 160 predicates defined as polytopes in about 30 minutes with less than 1GB memory [RMT13].


Resilience to Intermittent Assumption Violations in Reactive Synthesis

ExCAPE Researchers: Ehlers (Berkeley/Cornell), Topcu (Penn)

This project considers synthesis of reactive systems that are robust against intermittent violations of their environment assumptions. Such assumptions are needed to allow many systems that work in a larger context to fulfill their tasks. Yet, due to glitches in hardware or exceptional operating conditions, these assumptions do not always hold in the field. Building on generalized reactivity(1) synthesis, a synthesis approach that is well-known to be scalable enough for many practical applications, we show how, starting from a specification that is supported by this synthesis approach, we can modify it in order to use a standard generalized reactivity(1) synthesis procedure to find error-resilient systems. As an added benefit, this approach allows exploring the possible trade-offs in error resilience that a system designer has to make, and to give the designer a list of all Pareto-optimal implementations [EU14].


Synthesis of Insertion Functions for Enforcement of Opacity Security Properties

PI: Lafortune (Michigan)

We have investigated a new application domain for reactive synthesis techniques, namely, that of enforcement of security properties in networked systems. Specifically, we have considered the notion of opacity, which captures the ability, or lack thereof, of an intruder to infer a “secret” about a given system, based on its knowledge of the system structure and its observation of the system behavior. In cases where the desired opacity property does not hold, we have developed a novel synthesis methodology for the construction of a suitable interface, in the form of an insertion function, that provably enforces opacity by insertions of additional, fictitious, observable events. Our synthesis methodology is based on the construction of a finite structure that embeds all valid insertion functions. Game-theoretic results on weighted graphs can then be leveraged to synthesize optimal insertion functions when costs are assigned to the inserted events.We have shown how this methodology can be used to enforce privacy of the location of a user of location-based services [WL14].


Synthesis of State-Observers Resilient to Sensor Attacks

PI: Sangiovanni-Vincentelli (Berkeley), Seshia (Berkeley) and Tabuada (UCLA)

Motivated by the increasing number of reported attacks on cyber-physical systems (CPS), we are investigating the detection and mitigation of sensor attacks on CPS described by linear dynamics. In particular, our goal is to automatically synthesize algorithms that are able to isolate the sensors that have been compromised by an adversarial attack (detection) while being able to correctly estimate the state of the physical system (mitigation). Our approach combines Satisfiability Modulo Theory (SMT) solvers, convex optimization, and control theory to synthesize state estimators resilient to sensor attacks.


Papers:

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996