On Input Generators for Cyber-Physical Systems Falsification

被引:0
作者
Ramezani, Zahra [1 ]
Donze, Alexandre [2 ]
Fabian, Martin [1 ]
Akesson, Knut [1 ]
机构
[1] Chalmers Univ Technol, Dept Elect Engn, S-41718 Gothenburg, Sweden
[2] Decyphir SAS, Moirans, France
基金
瑞典研究理事会;
关键词
Generators; Semantics; Delays; Benchmark testing; Testing; Optimization; Pulse generation; Cyber-physical systems (CPSs); falsification; input generators; simulation-based optimization; testing;
D O I
10.1109/TCAD.2023.3333758
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Falsification is a testing method that aims to increase confidence in the correctness of cyber-physical systems by guiding the search for counterexamples with some optimization algorithm. This method generates input signals for a simulation of the system under test and employs quantitative semantics, which serves as objective functions, to minimize the distance needed to falsify a specification. Various implementations based on different optimization strategies and semantics have been proposed and evaluated in the past. Generally, they assume that an input generator is given. However, this is often not the case in practice and different choices can lead to vastly different outcomes. Therefore, this article introduces and evaluates various parameterizations of input generators, including pulse, sinusoidal, and piecewise signals with different interpolation techniques. These input generators are compared based on their performance on benchmark examples, as well as coverage measures in the space-time and frequency domains. Input generators facilitate the exploration of numerous different input signals within a single falsification problem, making them especially valuable for industrial practitioners seeking to incorporate falsification into their daily development work.
引用
收藏
页码:1274 / 1287
页数:14
相关论文
共 44 条
  • [1] Classification and Coverage-Based Falsification for Embedded Control Systems
    Adimoolam, Arvind
    Dang, Thao
    Donze, Alexandre
    Kapinski, James
    Jin, Xiaoqing
    [J]. COMPUTER AIDED VERIFICATION, CAV 2017, PT I, 2017, 10426 : 483 - 503
  • [2] Alur R, 2015, PRINCIPLES OF CYBER-PHYSICAL SYSTEMS, P1
  • [3] Annapureddy Y, 2011, LECT NOTES COMPUT SC, V6605, P254, DOI 10.1007/978-3-642-19835-9_21
  • [4] Falsification of Cyber-Physical Systems with Constrained Signal Spaces
    Barbot, Benoit
    Basset, Nicolas
    Dang, Thao
    Donze, Alexandre
    Kapinski, James
    Yamaguchi, Tomoya
    [J]. NASA FORMAL METHODS (NFM 2020), 2020, 12229 : 420 - 439
  • [5] Bracewell R., 1986, The Fourier transform and its applications
  • [6] ALMOST OPTIMAL SET COVERS IN FINITE VC-DIMENSION
    BRONNIMANN, H
    GOODRICH, MT
    [J]. DISCRETE & COMPUTATIONAL GEOMETRY, 1995, 14 (04) : 463 - 479
  • [7] QuickCheck: A lightweight tool for random testing of Haskell programs
    Claessen, K
    Hughes, J
    [J]. ACM SIGPLAN NOTICES, 2000, 35 (09) : 268 - 279
  • [8] Using Valued Booleans to Find Simpler Counterexamples in Random Testing of Cyber-Physical Systems
    Claessen, Koen
    Smallbone, Nicholas
    Eddeland, Johan
    Ramezani, Zahra
    Akesson, Knut
    [J]. IFAC PAPERSONLINE, 2018, 51 (07): : 408 - 415
  • [9] Stochastic Local Search for Falsification of Hybrid Systems
    Deshmukh, Jyotirmoy
    Jin, Xiaoqing
    Kapinski, James
    Maler, Oded
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 500 - 517
  • [10] Donzé A, 2010, LECT NOTES COMPUT SC, V6174, P167, DOI 10.1007/978-3-642-14295-6_17