BreachFlows: Simulation-Based Design with Formal Requirements for Industrial CPS (Extended Abstract)

Author Alexandre Donzé



PDF
Thumbnail PDF

File

OASIcs.ASD.2020.5.pdf
  • Filesize: 0.49 MB
  • 5 pages

Document Identifiers

Author Details

Alexandre Donzé
  • Decyphir SAS, Moirans, France

Cite AsGet BibTex

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)
https://doi.org/10.4230/OASIcs.ASD.2020.5

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering
  • Computer systems organization → Embedded and cyber-physical systems
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Streaming models
  • Mathematics of computing → Solvers
  • Computing methodologies → Model verification and validation
  • Computing methodologies → Simulation evaluation
  • Computing methodologies → Simulation tools
  • Computing methodologies → Machine learning
  • Software and its engineering → Software creation and management
  • Theory of computation → Mathematical optimization
Keywords
  • Cyber Physical Systems
  • Verification and Validation
  • Test
  • Model-Based Design
  • Formal Requirements
  • Falsification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Koen Claessen, Nicholas Smallbone, Johan Liden Eddeland, Zahra Ramezani, Knut Åkesson, and Sajed Miremadi. Applying valued booleans in testing of cyber-physical systems. In MT@CPSWeek, pages 8-9. IEEE, 2018. Google Scholar
  2. Jyotirmoy V. Deshmukh, Xiaoqing Jin, James Kapinski, and Oded Maler. Stochastic local search for falsification of hybrid systems. In ATVA, volume 9364 of Lecture Notes in Computer Science, pages 500-517. Springer, 2015. Google Scholar
  3. Alexandre Donzé. Breach, A toolbox for verification and parameter synthesis of hybrid systems. In Proc. of CAV 2010: the 22nd International Conference on Computer Aided Verification, volume 6174 of LNCS, pages 167-170. Springer, 2010. Google Scholar
  4. Alexandre Donzé, Thomas Ferrère, and Oded Maler. Efficient robust monitoring for STL. In Proc. of CAV 2013: the 25th International Conference on Computer Aided Verification, volume 8044 of LNCS, pages 264-279. Springer, 2013. Google Scholar
  5. Tommaso Dreossi, Alexandre Donzé, and Sanjit A. Seshia. Compositional falsification of cyber-physical systems with machine learning components. J. Autom. Reasoning, 63(4):1031-1053, 2019. URL: https://doi.org/10.1007/s10817-018-09509-5.
  6. Mathworks Inc. Test generated code with sil and pil simulations. Cf. URL: https://www.mathworks.com/help/ecoder/examples/software-and-processor-in-the-loop-sil-and-pil-simulation.html.
  7. Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In FORMATS/FTRTFT, pages 152-166, 2004. Google Scholar
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