Search Results

Documents authored by Donzé, Alexandre

Document
Extended Abstract
DOI: 10.4230/OASIcs.ASD.2020.5
BreachFlows: Simulation-Based Design with Formal Requirements for Industrial CPS (Extended Abstract)

Authors: Alexandre Donzé

Published in: OASIcs, Volume 79, 2nd International Workshop on Autonomous Systems Design (ASD 2020)

Abstract
Cyber-Physical Systems (CPS) are computerized systems in interaction with their physical environment. They are notoriously difficult to design because their programming must take into account these interactions which are, by nature, a mix of discrete, continuous and real-time behaviors. As a consequence, formal verification is impossible but for the simplest CPS instances, and testing is used extensively but with little to no guarantee. Falsification is a type of approach that goes beyond testing in the direction of a more formal methodology. It has emerged in the recent years with some success. The idea is to generate input signals for the system, monitor the output for some requirements of interest, and use black-box optimization to guide the generation toward an input that will falsify, i.e., violate, those requirements. Breach is an open source Matlab/Simulink toolbox that implements this approach in a modular and extensible way. It is used in academia as well as for industrial applications, in particular in the automotive domain. Based on experience acquired during close collaborations between academia and industry, Decyphir is developing BreachFlows, and extension/front-end for Breach which implements features that are required or useful in an industrial context.
Cite as

Alexandre Donzé. BreachFlows: Simulation-Based Design with Formal Requirements for Industrial CPS (Extended Abstract). In 2nd International Workshop on Autonomous Systems Design (ASD 2020). Open Access Series in Informatics (OASIcs), Volume 79, pp. 5:1-5:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{donze:OASIcs.ASD.2020.5,
  author =	{Donz\'{e}, Alexandre},
  title =	{{BreachFlows: Simulation-Based Design with Formal Requirements for Industrial CPS}},
  booktitle =	{2nd International Workshop on Autonomous Systems Design (ASD 2020)},
  pages =	{5:1--5:5},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-141-2},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{79},
  editor =	{Steinhorst, Sebastian and Deshmukh, Jyotirmoy V.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ASD.2020.5},
  URN =		{urn:nbn:de:0030-drops-125995},
  doi =		{10.4230/OASIcs.ASD.2020.5},
  annote =	{Keywords: Cyber Physical Systems, Verification and Validation, Test, Model-Based Design, Formal Requirements, Falsification}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.463
Control Improvisation

Authors: Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia, and David Wessel

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We formalize and analyze a new automata-theoretic problem termed control improvisation. Given an automaton, the problem is to produce an improviser, a probabilistic algorithm that randomly generates words in its language, subject to two additional constraints: the satisfaction of an admissibility predicate, and the exhibition of a specified amount of randomness. Control improvisation has multiple applications, including, for example, generating musical improvisations that satisfy rhythmic and melodic constraints, where admissibility is determined by some bounded divergence from a reference melody. We analyze the complexity of the control improvisation problem, giving cases where it is efficiently solvable and cases where it is #P-hard or undecidable. We also show how symbolic techniques based on Boolean satisfiability (SAT) solvers can be used to approximately solve some of the intractable cases.
Cite as

Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia, and David Wessel. Control Improvisation. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 463-474, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{fremont_et_al:LIPIcs.FSTTCS.2015.463,
  author =	{Fremont, Daniel J. and Donz\'{e}, Alexandre and Seshia, Sanjit A. and Wessel, David},
  title =	{{Control Improvisation}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{463--474},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.463},
  URN =		{urn:nbn:de:0030-drops-56596},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.463},
  annote =	{Keywords: finite automata, random sampling, Boolean satisfiability, testing, computational music, control theory}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact