Designers of industrial embedded control systems, such as automotive, aerospace, and medical-device control systems, use verification and testing activities to increase their confidence that performance requirements and safety standards are met. Since testing and verification tasks account for a significant portion of the development effort, increasing the efficiency of testing and verification will have a significant impact on the total development cost. Existing and emerging simulation-based approaches offer improved means of testing and, in some cases, verifying the correctness of control system designs.

We extend our CAV 2015 paper with a different algorithm for computing Skorokhod distance. The key assumption for this algorithm is that traces are now sampled at a greater frequency, allowing a simpler piecewise-constant interpolation scheme to be used to interpret traces. The paper studies the tradeoff between the sampling frequency and the computational efficiency of the new algorithm. The paper also extends transference results to TPTL that allows freeze quantifiers in the value domain.

Journal version of the ESOP 2010 paper. Derives concurrency control for a sequential library to make it thread-safe, given proof of sequential correctness of the library. Thread safety defined as: a) absence of assertion failures in concurrent context, or b) linearizability of library.

Extended version of the ASE 09 paper. Also presents a new static analysis for deadlocks arising from wait-notify based synchronization in programs using nested monitors.

Evaluation of industrial embedded control system designs is a time-consuming and imperfect process. While an ideal process would apply a formal verification technique such as model checking or theorem proving, these techniques do not scale to industrial design problems, and it is often difficult to use these techniques to verify performance aspects of control system designs, such as stability or convergence. For industrial designs, engineers rely on testing processes to identify critical or unexpected behaviors. We propose a novel framework called Underminer to improve the testing process; this is an automated technique to identify non-converging behaviors in embedded control system designs. Underminer treats the system as a black box, and lets the designer indicate the model parameters, inputs and outputs that are of interest. It supports a multiplicity of convergence-like notions, such as those based on Lyapunov analysis and those based on temporal logic formulae. Underminer can be applied in the context of testing models created in the controller-design phase, and can also be applied in a scenario such as hardware-in-the-loop testing. We demonstrate the efficacy of Underminer by evaluating its performance on several examples.

We study the problem of falsifying reachability properties of real-time control software acting in a closed-loop with a given model of the plant dynamics. Our approach employs numerical techniques to simulate a plant model, which may be highly nonlinear and hybrid, in combination with symbolic simulation of the controller software. The state-space and input-space of the plant are systematically searched using a plant abstraction that is implicitly defined by ``quantization'' of the plant state, but never explicitly constructed. Simultaneously, the controller behaviors are explored using a symbolic execution of the control software. On-the-fly exploration of the overall closed-loop abstraction results in abstract counterexamples, which are used to refine the plant abstraction iteratively until a concrete violation is found. Empirical evaluation of our approach shows its promise in treating controller software that has precise, formal semantics, using an exact method such as symbolic execution, while using numerical simulations to produce abstractions of the underlying plant model that is often an approximation of the actual plant. We also discuss a preliminary comparison of our approach with techniques that are primarily simulation-based.

Forward invariant cuts are invariant and safe sets that may not be initialized. This paper introduces the forward invariant cut rule in the calculus of the KeYmaera theorem prover. It also suggests how designers could translate localized design information (about a given discrete mode, or a set of modes), into a forward invariant cut, that helps simplify the proof of system safety (by eliminating parts of the hybrid state space).

Signal Temporal Logic allows specifying temporal properties of real-valued signals over dense time-domains. Alongwith the usual Boolean semantics, it is also equipped with quantitative semantics that allow estimating how robustly a given signal satisfies a given property. Offline algorithms to compute the robust satisfaction value require the entire signal over a given finite time horizon to be available before computation can proceed. Online algorithms can estimate upper and lower bounds on the robust satisfaction value (called the robust satisfaction interval RoSI) over prefixes of a complete signal, updating the RoSI as more information about the signal becomes available. In this paper, we propose memory-efficient algorithms to monitor the RoSI in an online fashion.

The Skorokhod distance is a metric on functions (over time) that quantifies mismatches between signal values as well as time jitter. This metric has been heretofore used to define topologies for hybrid systems, but Vinayak and Rupak had a nice paper in HSCC 2015 to compute the Skorokhod distance for polygonal traces in polynomial time. We employ this a metric for testing conformance. First, we explore a restriction of the metric which restricts time jitter to a finite window -- this brings down the complexity to linear in the length of the trace. Next, we explore an optimization-guided approach to find an input to two dynamical systems that maximizes the Skorokhod distance between the corresponding outputs. This corresponds to finding non-conformant behavior. Finally, we show that traces satisfying similar temporal logic properties are classified to be close by the Skorokhod metric; further establishing its usefulness in quantifying system conformance.

We present an approach that uses Rapidly Exploring Random Trees (RRTs) to explore the state space of a dynamical system, with the dual objective of maximimizing the coverage (measured using the star-discrepancy metric), and minimizing the robust satisfaction value of a given Signal Temporal Logic requirement. In other words, a bug-finding technique guided by robustness and coverage.

Contraction metrics help establish incremental stability of dynamical systems. We present a simulation-guided technique to discover contraction metrics for highly nonlinear systems.

We present an approach for finding violations of safety properties of hybrid systems. Existing approaches search for complete system trajectories that begin from an initial state and reach some unsafe state. Our approach searches over sequences of trajectory segments starting from any system states, where adjacent segments may have gaps; our approach then seeks to narrow these gaps iteratively. Interesting segmented trajectories are discovered using a randomized scatter-and-simulate algorithm.

We present a technique that allows us to find Sum-of-Squares Lyapunov functions for hybrid dynamical systems. Given a template form for the Lyapunov function, our technique uses simulation data to infer constraints, the solution of which provides a candidate Lyapunov function. Our technique then uses a global optimizer to search the region of interest for trajectories that violate the Lyapunov conditions for the given function, which are fed back into the procedure as additional constraints. Once the procedure terminates, we use a nonlinear SMT solver to verify the Lyapunov conditions, in order to obtain a proof of soundness of the candidate Lyapunov function (which the global optimizer cannot guarantee). Failures of this check give yet another set of constraints to drive the search procedure.

We present models for an important problem in the automotive domain of powertrain control -- that of air-fuel ratio control. The first and the most complex model consists of a plant model that is a dynamical system capturing the physical behavior of important subsystems in the engine and a multi-mode controller representing different regimes of operation. The second and third model are successive simplifications of the first, and hope to present the research community with manageable benchmark problems for verification and analysis tools. We also present a suite of interesting requirements for these models expressed in a temporal logic over real-valued signals and dense time.

We present a technique that allows us to find Sum-of-Squares Lyapunov functions for nonlinear discrete dynamical systems. Given a template form for the Lyapunov function, our technique uses simulation data to infer constraints, the solution of which provides a candidate Lyapunov function. Our technique then uses a global optimizer to search the region of interest for trajectories that violate the Lyapunov conditions for the given function, which are fed back into the procedure as additional constraints. We derive conditions involving the Lipschitz constants of the vector field and the Lyapunov candidate function, and a sampling density that guarantee that testing the Lyapunov conditions at each point in the random sampling of the region of interest is sufficient to prove the validity of the Lyapunov function over the entire region.

Usual falsification techniques search for simulation traces violating a given safety property by sequential search. We explore the idea of using a global optimizer to minimize the distance between end-points of trajectory segments thereby approaching a real trajectory. Such directionless search has the potential to search the state-space in a less restricted fashion, and thus more comprehensively for systems with large amounts of switching.

Over a chosen metric topology, we define a transducer as robust if bounded distance input strings have bounded distance outputs. Algorithms based on checking emptiness of automata are presented for robustness analysis of transducers over the metric space induced by the Manhattan distance and the one induced by Levenshtein or edit distance.

The theory of regular functions provides a class of analyzable functions from strings to numbers, that can provide a foundation for analyzing quantitative properties of finite-state sysmtes. Cost Register Automata (CRA) are deterministic machines that map strings to costs using a vocabulary of interesting operations such as adding, scaling, min. The notion of regularity provides a yardstick to measure expressiveness, and to study decision problems and theoretical properties of resulting classes of cost functions. Over suitably defined vocabularies, CRA generalize weighted automata and probabilistic automata, and also allow us to express generalized min-cost problems over directed graphs.

Requirements for industrial control systems are often imprecise, non-modular, evolving, or even simply unknown. We propose a framework for automatically mining requirements from Simulink models. The input to our algorithm is a requirement template expressed in Parametric Signal Temporal Logic. Our algorithm is an instance of counterexample-guided inductive synthesis: an intermediate candidate requirement is synthesized from simulation traces of the system, which is refined using counterexamples to the candidate obtained with the help of a falsification tool.

We propose a new design methodology for communication protocols based on the observation that protocols are usually understood in terms of abstract scenarios; each of which consists of a set of transition snippets. A transition snippet describes a single step of the concrete behavior of a protocol, or a single symbolic execution step, or a mixture of both. Given a protocol specified as snippets, we show how intelligent expression and synthesis coupled with an explicit-state model checker can be used in an iterative manner to converge to a complete, fully symbolic protocol description. The advantage of doing things this way is twofold: (1) specifying a protocol as scenarios is more natural, and (2) our synthesis procedure provides a correct-by-construction protocol from such a designer-friendly specification.

We present a notion of robustness for a networked system when the underlying network is prone to errors. Networked system is modeled as Mealy machines communicating over a set of internal channels, and interacting with the outside world through a fixed set of input and output channels. We focus on network errors that arise from channel perturbations, and given a worst-case bound 'i' for the number of errors that can occur in the internal channels, we estimate if the worst-case error in the output channel is less than a given bound 'o'. Such a network is called (i,o)-robust. Error is measured as distance from unperturbed output, and we give procedures polynomial in the size of the network when the distance metric is the edit (Levenshtein) distance or the L1-norm.

NSSTs can realize MSO-definable relations between strings, and are closed under seq. composition. Functional NSSTs are nondeterministic, yet implement functions from strings to strings. Checking functionality of an NSST is in PSPACE, equivalence checking for functional NSSTs is PSPACE-complete, while that for NSSTs is undecidable. Checking containment of an NSST in a finite union of deterministic SSTs is in PSPACE. An NSST could be potentially used as a model for concurrent methods acting on a singly-linked data structure.

We address two problems: (1) Given an input structure, transform it in a cost-efficient fashion to make sure that the output satisfies properties of interest, (2) Given a class of structures, synthesize a small program to uniformly transform them to a desired class of outputs.

Derives concurrency control for a sequential library to make it thread-safe, given proof of sequential correctness of the library. Thread safety defined as: a) absence of assertion failures in concurrent context, or b) linearizability of library.

Identifies syntactic fragment and associated sufficient conditions such that recursive methods therein can be algorithmically verified. Methods and pre/post- conditions encoded as tree automata; correctness reduced to language emptiness.

Derives interface contracts over concurrent invocations of library methods to ensure deadlock-freedom. Symbolcally explores the exponential number of alias patterns across method arguments, using a SMT solver to derive contracts in terms of these patterns.

For Boolean Programs specified by pre/post-condition semantics, uses local annotations generated by pre/post-condition propagation to generate repairs. Improves on existing complexity results by an intelligent repair extraction.

Reduces verification of parameterized data structures to the emptiness of tree automata. Can verify properties like acyclicity for a reasonable set of methods operating on lists, trees, and general graphs.

We present results of comparing two different techniques for obtaining PWA approximations of nonlinear dynamical systems on a powertrain control benchmark model.

We present an extension to the deductive verification framework of differential dynamic logic that allows the theorem prover KeYmaera to locally reason about behaviors by leveraging forward invariant sets provided by external methods, such as numerical techniques and designer insights.

We present an enhanced version of the benchmark models presented in HSCC 2014. We place emphasis on comparing the models on standard control-theoretic metrics, and suggest future directions where model transformations could be guided by the necessity for transformed models to be conformant.