| 1. |
- Lidén Eddeland, Johan, 1991, et al.
(author)
-
Industrial Temporal Logic Specifications for Falsification of Cyber-Physical Systems
- 2020
-
In: EPiC Series in Computing. - : EasyChair. - 2398-7340. ; 74, s. 267-274
-
Conference paper (peer-reviewed)abstract
- In this benchmark proposal, we present a set of large specifications stated in Signal Temporal Logic (STL) intended for use in falsification of Cyber-Physical Systems. The main purpose of the benchmark is for tools that monitor STL specifications to be able to test their performance on complex specifications that have structure similar to industrial specifications. The benchmark itself is a Git repository which will therefore be updated over time, and new specifications can be added. At the time of submission, the repository contains a total of seven Simulink requirement models, resulting in 17 generated STL specifications.
|
|
| 2. |
- Lidén Eddeland, Johan, 1991, et al.
(author)
-
Multi-Requirement Testing Using Focused Falsification
- 2022
-
In: HSCC 2022 - Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control, Part of CPS-IoT Week 2022. - New York, NY, USA : ACM.
-
Conference paper (peer-reviewed)abstract
- Testing of Cyber-Physical Systems (CPS) deals with the problem of finding input traces to the systems such that given requirements do not hold. Requirements can be formalized in many different ways; in this work requirements are modeled using Signal Temporal Logic (STL) for which a quantitative measure, or \emph{robustness value}, can be computed given a requirement together with input and output traces. This value is a measure of how far away the requirement is from not holding and is used to guide falsification procedures for deciding on new input traces to simulate one after the other. When the system under test has multiple requirements, standard approaches are to falsify them one-by-one, or as a conjunction of all requirements, but these approaches do not scale well for industrial-sized problems. In this work we consider testing of systems with multiple requirements by proposing focused multi-requirement falsification. This is a multi-stage approach where the solver tries to sequentially falsify the requirements one-by-one, but for every simulation also evaluate the robustness value for all requirements. After one requirement has been focused long enough, the next requirement to focus is selected by considering the robustness values and trajectory history calculated thus far. Each falsification attempt makes use of a prior sensitivity analysis, which for each requirement estimates the parameters that are unlikely to affect the robustness value, in order to reduce the number of parameters that are used by the optimization solver. The proposed approach is evaluated on a public benchmark example containing a large number of requirements, and includes a comparison of the proposed algorithm against a new suggested baseline method.
|
|
| 3. |
- Ramezani, Zahra, 1988, et al.
(author)
-
On Input Generators for Cyber-Physical Systems Falsification
- 2024
-
In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. - 1937-4151 .- 0278-0070. ; 43:4, s. 1274-1287
-
Journal article (peer-reviewed)abstract
- This method generates input signals to a simulation of the system under test and uses quantitative semantics that plays the role of objective functions to minimize the distance to falsify a specification. This paper presents and evaluates differently structured parameterizations of input generators: pulse, sinusoidal, and piecewise with different interpolation signals. The input generators are compared based on their results on benchmark examples, as well as coverage measures in the space and time, and frequency domains. Input generators allow covering many different input signals in a single falsification problem, which is especially useful for industrial practitioners wanting to use falsification in their daily development work. Falsification is a testing method that aims to increase confidence in the correctness of cyber-physical systems by searching for counterexamples guided by an optimization algorithm. This method generates input signals for a simulation of the system under test and employs quantitative semantics, which serve as objective functions, to minimize the distance needed to falsify a specification. This paper introduces and evaluates various parameterizations of input generators, including pulse, sinusoidal, and piecewise signals with different interpolation techniques. The 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 enable the exploration of numerous different input signals within a single falsification problem, making them particularly valuable for industrial practitioners who wish to incorporate falsification into their daily development work.
|
|
| 4. |
- Ramezani, Zahra, 1988, et al.
(author)
-
Temporal Logic Falsification of Cyber-Physical Systems using Input Pulse Generators
- 2021
-
In: EPiC Series in Computing. - : EasyChair. - 2398-7340. ; 80, s. 195-202
-
Conference paper (peer-reviewed)abstract
- Falsification is a testing method for cyber-physical systems where numerical optimization is used to find counterexamples of a given specification that the system must fulfill. The falsification process uses quantitative semantics that play the role of objective functions to minimize the distance to falsifying the specification. Falsification has gained attention due to its versatile applicability, and much work exists on various ways of implementing the falsification process, often focusing on which optimization algorithm to use, or more recently, the semantics for the formal requirements. In this work, we look at some practical aspects of input generation, i.e., the mapping from parameters used as optimization variables to signals that form the actual test cases for the system. This choice is critical but often overlooked. It is assumed that problem experts can guide how to parameterize inputs; however, this assumption is often too optimistic in practice. We observe that pulse generation is a surprisingly good first option that can falsify many common benchmarks after only a few simulations while requiring only a few parameters per signal.
|
|
