TY - GEN
T1 - Efficient Optimization-Based Falsification of Cyber-Physical Systems with Multiple Conjunctive Requirements
AU - Mathesen, Logan
AU - Pedrielli, Giulia
AU - Fainekos, Georgios
N1 - Funding Information:
* Logan Mathesen is supported as a NSF Graduate Research Fellow, grant number 026257-001. This research has also been partially supported by NSF CNS 1932068.
Funding Information:
The research in this paper has been partially supported by the grant DARPA FA8750-20-C-0507, NSF #2046588, and NSF #1829238.
Publisher Copyright:
© 2021 IEEE.
PY - 2021/8/23
Y1 - 2021/8/23
N2 - Optimization-based falsification, or search-based testing, is a method of automatic test generation for Cyber-Physical System (CPS) safety evaluation. CPS safety evaluation is guided by high level system requirements that are expressed in Signal Temporal Logic (STL). Trajectories from executed CPS simulations are evaluated against STL requirements using satisfaction robustness as a quantitative metric. In particular, robustness is the distance metric between the simulated system trajectory, associated to a specific input, and the known unsafe set, i.e., regions of the search space that violate the requirements. Identification of violations can be formulated as an optimization problem, where inputs that minimize the robustness function are of interest. In fact, an input falsifies a requirement if the associated robustness is negative. In this work, specifically, we consider the case where multiple requirements determine the unsafe set. Due to the computational burden of executing CPS simulations, practitioners often test all system requirements simultaneously by combining the requirement components and obtaining so-called 'conjunctive requirements'. Conjunctive requirements can challenge optimization-based falsification approaches due to the fact that the robustness function may 'mask' the contributions of individual conjunctive requirement components. We propose a new algorithm, minimum Bayesian optimization (minBO), that deals with this problem by considering the contributions of each component of the conjunctive requirement. We show the advantages of the minBO optimization algorithm when applied to general non-linear non-convex optimization problems as well as when applied to realistic falsification applications.
AB - Optimization-based falsification, or search-based testing, is a method of automatic test generation for Cyber-Physical System (CPS) safety evaluation. CPS safety evaluation is guided by high level system requirements that are expressed in Signal Temporal Logic (STL). Trajectories from executed CPS simulations are evaluated against STL requirements using satisfaction robustness as a quantitative metric. In particular, robustness is the distance metric between the simulated system trajectory, associated to a specific input, and the known unsafe set, i.e., regions of the search space that violate the requirements. Identification of violations can be formulated as an optimization problem, where inputs that minimize the robustness function are of interest. In fact, an input falsifies a requirement if the associated robustness is negative. In this work, specifically, we consider the case where multiple requirements determine the unsafe set. Due to the computational burden of executing CPS simulations, practitioners often test all system requirements simultaneously by combining the requirement components and obtaining so-called 'conjunctive requirements'. Conjunctive requirements can challenge optimization-based falsification approaches due to the fact that the robustness function may 'mask' the contributions of individual conjunctive requirement components. We propose a new algorithm, minimum Bayesian optimization (minBO), that deals with this problem by considering the contributions of each component of the conjunctive requirement. We show the advantages of the minBO optimization algorithm when applied to general non-linear non-convex optimization problems as well as when applied to realistic falsification applications.
UR - http://www.scopus.com/inward/record.url?scp=85117030289&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85117030289&partnerID=8YFLogxK
U2 - 10.1109/CASE49439.2021.9551474
DO - 10.1109/CASE49439.2021.9551474
M3 - Conference contribution
AN - SCOPUS:85117030289
T3 - IEEE International Conference on Automation Science and Engineering
SP - 732
EP - 737
BT - 2021 IEEE 17th International Conference on Automation Science and Engineering, CASE 2021
PB - IEEE Computer Society
T2 - 17th IEEE International Conference on Automation Science and Engineering, CASE 2021
Y2 - 23 August 2021 through 27 August 2021
ER -