We consider the problem of generating input signals for validation of cyber-physical systems. The class of signals that we are interested in is subject to complex constraints in both time and value domains, which are captured by Symbolic Timed Automata (STA). We propose a method for uniform sampling of traces recognised by STA. The proposed procedure is general and works for arbitrary alphabets equipped with a probability space and a computable measure. We devise a concrete method for linear alphabets. We then show how this method can be used to enhance falsification based on both sampling and optimisation. The results are validated on the case study of an artificial pancreas.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Signal Sampling and Optimisation Under Symbolic Timed Automata Constraints

  • Benoît Barbot,
  • Nicolas Basset,
  • Thao Dang,
  • Alexandre Donzé,
  • Marco Esposito,
  • Dejan Nickovic

摘要

We consider the problem of generating input signals for validation of cyber-physical systems. The class of signals that we are interested in is subject to complex constraints in both time and value domains, which are captured by Symbolic Timed Automata (STA). We propose a method for uniform sampling of traces recognised by STA. The proposed procedure is general and works for arbitrary alphabets equipped with a probability space and a computable measure. We devise a concrete method for linear alphabets. We then show how this method can be used to enhance falsification based on both sampling and optimisation. The results are validated on the case study of an artificial pancreas.