-
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
Authors:
Tommaso Dreossi,
Alexandre Donzé,
Sanjit A. Seshia
Abstract:
Cyber-physical systems (CPS), such as automotive systems, are starting to include sophisticated machine learning (ML) components. Their correctness, therefore, depends on properties of the inner ML modules. While learning algorithms aim to generalize from examples, they are only as good as the examples provided, and recent efforts have shown that they can produce inconsistent output under small ad…
▽ More
Cyber-physical systems (CPS), such as automotive systems, are starting to include sophisticated machine learning (ML) components. Their correctness, therefore, depends on properties of the inner ML modules. While learning algorithms aim to generalize from examples, they are only as good as the examples provided, and recent efforts have shown that they can produce inconsistent output under small adversarial perturbations. This raises the question: can the output from learning components can lead to a failure of the entire CPS? In this work, we address this question by formulating it as a problem of falsifying signal temporal logic (STL) specifications for CPS with ML components. We propose a compositional falsification framework where a temporal logic falsifier and a machine learning analyzer cooperate with the aim of finding falsifying executions of the considered model. The efficacy of the proposed technique is shown on an automatic emergency braking system model with a perception component based on deep neural networks.
△ Less
Submitted 16 December, 2018; v1 submitted 2 March, 2017;
originally announced March 2017.
-
Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems
Authors:
Tommaso Dreossi
Abstract:
Sapo is a C++ tool for the formal analysis of polynomial dynamical systems. Its main features are: 1) Reachability computation, i.e., the calculation of the set of states reachable from a set of initial conditions, and 2) Parameter synthesis, i.e., the refinement of a set of parameters so that the system satisfies a given specification. Sapo can represent reachable sets as unions of boxes, paralle…
▽ More
Sapo is a C++ tool for the formal analysis of polynomial dynamical systems. Its main features are: 1) Reachability computation, i.e., the calculation of the set of states reachable from a set of initial conditions, and 2) Parameter synthesis, i.e., the refinement of a set of parameters so that the system satisfies a given specification. Sapo can represent reachable sets as unions of boxes, parallelotopes, or parallelotope bundles (symbolic representation of polytopes). Sets of parameters are represented with polytopes while specifications are formalized as Signal Temporal Logic (STL) formulas.
△ Less
Submitted 7 July, 2016;
originally announced July 2016.
-
Falsifying Oscillation Properties of Parametric Biological Models
Authors:
Thao Dang,
Tommaso Dreossi
Abstract:
We propose an approach to falsification of oscillation properties of parametric biological models, based on the recently developed techniques for testing continuous and hybrid systems. In this approach, an oscillation property can be specified using a hybrid automaton, which is then used to guide the exploration in the state and input spaces to search for the behaviors that do not satisfy the prop…
▽ More
We propose an approach to falsification of oscillation properties of parametric biological models, based on the recently developed techniques for testing continuous and hybrid systems. In this approach, an oscillation property can be specified using a hybrid automaton, which is then used to guide the exploration in the state and input spaces to search for the behaviors that do not satisfy the property. We illustrate the approach with the Laub-Loomis model for spontaneous oscillations during the aggregation stage of Dictyostelium.
△ Less
Submitted 3 September, 2013;
originally announced September 2013.
-
Approximated Symbolic Computations over Hybrid Automata
Authors:
Alberto Casagrande,
Tommaso Dreossi,
Carla Piazza
Abstract:
Hybrid automata are a natural framework for modeling and analyzing systems which exhibit a mixed discrete continuous behaviour. However, the standard operational semantics defined over such models implicitly assume perfect knowledge of the real systems and infinite precision measurements. Such assumptions are not only unrealistic, but often lead to the construction of misleading models. For these…
▽ More
Hybrid automata are a natural framework for modeling and analyzing systems which exhibit a mixed discrete continuous behaviour. However, the standard operational semantics defined over such models implicitly assume perfect knowledge of the real systems and infinite precision measurements. Such assumptions are not only unrealistic, but often lead to the construction of misleading models. For these reasons we believe that it is necessary to introduce more flexible semantics able to manage with noise, partial information, and finite precision instruments. In particular, in this paper we integrate in a single framework based on approximated semantics different over and under-approximation techniques for hybrid automata. Our framework allows to both compare, mix, and generalize such techniques obtaining different approximated reachability algorithms.
△ Less
Submitted 24 August, 2013;
originally announced August 2013.
