| 1. |
- Claessen, Koen, 1975, et al.
(författare)
-
Applying valued booleans in testing of cyber-physical systems
- 2018
-
Ingår i: Proceedings - 2018 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT-CPS 2018. ; , s. 8-9
-
Konferensbidrag (refereegranskat)abstract
- In software testing, as in cyber-physical systems testing, test suites are traditionally developed by hand. In this work we consider one framework for putting the computer in charge of the testing instead: constrained random test case generation as supported by the tool QuickCheck. This is implemented by the use of Valued Booleans (VBools). VBools naturally allow for an extension of QuickCheck into cyber-physical systems, which is useful particularly since QuickCheck can perform shrinking of test cases. Shrinking is a technique to make test cases simpler while preserving failure.
|
|
| 2. |
- Lidén Eddeland, Johan, 1991, et al.
(författare)
-
Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans
- 2020
-
Ingår i: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. - 1937-4151 .- 0278-0070. ; 39:12, s. 5247-5260
-
Tidskriftsartikel (refereegranskat)abstract
- Cyber-Physical Systems (CPSs) are systems with both physical and software components, for example cars and industrial robots. Since these systems exhibit both discrete and continuous dynamics, they are complex and it is thus difficult to verify that they behave as expected. Falsification of temporal logic properties is an approach to find counterexamples to CPSs by means of simulation. In this paper, we propose two additions to enhance the capability of falsification and make it more viable in a large-scale industrial setting. The first addition is a framework for transforming specifications from a signal-based model into Signal Temporal Logic. The second addition is the use of Valued Booleans and an additive robust semantics in the falsification process. We evaluate the performance of the additive robust semantics on a set of benchmark models, and we can see that which semantics are preferable depend both on the model and on the specification.
|
|
| 3. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Using Valued Booleans to Find Simpler Counterexamples in Random Testing of Cyber-Physical Systems
- 2018
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 51:7, s. 408-415
-
Konferensbidrag (refereegranskat)abstract
- We propose a new logic of valued Booleans for writing properties which are not just true or false but compute how severely they are falsified. The logic is reminiscent of STL or MTL but gives the tester control over what severity means in the particular problem domain. We use this logic to simplify failing test inputs in the context of random testing of cyber-physical systems and show that it improves the quality of counterexamples found. The logic of valued Booleans might also be used as an alternative to the standard robust semantics of STL formulas in optimization-based approaches to falsification.
|
|
| 4. |
- Ramezani, Zahra, 1988, et al.
(författare)
-
Comparative Case Studies of Reactive Synthesis and Supervisory Control
- 2019
-
Ingår i: 2019 18th European Control Conference, ECC 2019. ; , s. 1752-1759
-
Konferensbidrag (refereegranskat)abstract
- Reactive Synthesis and Supervisory Control Theory are both systematic approaches for the automatic construction of controllers from requirements. However, their underlying technicalities differ significantly. This paper provides an empirical comparison between these two approaches from the modelling perspective through case studies. Using the synthesis tools TuLiP and Supremica, two examples are modelled in the typical modelling formalism supported by each tool, and the algorithms are applied to synthesize controllers. Based on the obtained models and experiences, we compare how the models are derived, and how the characteristics of the examples and the underlying synthesis algorithms influence the modelling choices.
|
|
| 5. |
- Ramezani, Zahra, 1988
(författare)
-
Enhancing Temporal Logic Falsification of Cyber-Physical Systems using multiple objective functions and a new optimization method
- 2020
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Cyber-physical systems (CPSs) are engineering systems that bridge the cyber-world of communications and computing with the physical world. These systems are usually safety-critical and exhibit both discrete and continuous dynamics that may have complex behavior. Typically, these systems have to satisfy given specifications, i.e., properties that define the valid behavior. One commonly used approach to evaluate the correctness of CPSs is testing. The main aim of testing is to detect if there are situations that may falsify the specifications. For many industrial applications, it is only possible to simulate the system under test because mathematical models do not exist, thus formal verification is not a viable option. Falsification is a strategy that can be used for testing CPSs as long as the system can be simulated and formal specifications exist. Falsification attempts to find counterexamples, in the form of input signals and parameters, that violate the specifications of the system. Random search or optimization can be used for the falsification process. In the case of an optimization-based approach, a quantitative semantics is needed to associate a simulation with a measure of the distance to a specification being falsified. This measure is used to guide the search in a direction that is more likely to falsify a specification, if possible. The measure can be defined in different ways. In this thesis, we evaluate different quantitative semantics that can be used to define this measure. The efficiency of the falsification can be affected by both the quantitative semantics used and the choice of the optimization method. The presented work attempts to improve the efficiency of the falsification process by suggesting to use multiple quantitative semantics, as well as a new optimization method. The use of different quantitative semantics and the new optimization method have been evaluated on standard benchmark problems. We show that the proposed methods improve the efficiency of the falsification process.
|
|
| 6. |
- Ramezani, Zahra, 1988, et al.
(författare)
-
Evaluating Two Semantics for Falsification using an Autonomous Driving Example
- 2019
-
Ingår i: IEEE International Conference on Industrial Informatics (INDIN). - 1935-4576. - 9781728129273 ; 2019-July, s. 386-391
-
Konferensbidrag (refereegranskat)abstract
- We consider the falsification of temporal logic properties as a method to test complex systems, such as autonomous systems. Since these systems are often safety-critical, it is important to assess whether they fulfill given specifications or not. An adaptive cruise controller for an autonomous car is considered where the closed-loop model has unknown parameters and an important problem is to find parameter combinations for which given specification are broken. We assume that the closed-loop system can be simulated with the known given parameters, no other information is available to the testing framework. The specification, such as, the ability to avoid collisions, is expressed using Signal Temporal Logic (STL). In general, systems consist of a large number of parameters, and it is not possible or feasible to explicitly enumerate all combinations of the parameters. Thus, an optimization-based approach is used to guide the search for parameters that might falsify the specification. However, a key challenge is how to select the objective function such that the falsification of the specification, if it can be falsified, can be falsified using as few simulations as possible. For falsification using optimization it is required to have a measure representing the distance to the falsification of the specification. The way the measure is defined results in different objective functions used during optimization. Different measures have been proposed in the literature and in this paper the properties of the Max Semantics (MAX) and the Mean Alternative Robustness Value (MARV) semantics are discussed. After evaluating these two semantics on an adaptive cruise control example, we discuss their strengths and weaknesses to better understand the properties of the two semantics.
|
|
| 7. |
- Ramezani, Zahra, 1988, et al.
(författare)
-
Multiple Objective Functions for Falsification of Cyber-Physical Systems
- 2020
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 53:4, s. 417-422
-
Konferensbidrag (refereegranskat)abstract
- Cyber-physical systems are typically safety-critical, thus it is crucial to guarantee that they conform to given specifications, that are the properties that the system must fulfill. Optimization-based falsification is a model-based testing method to find counterexamples of the specifications. The main idea is to measure how far away a specification is from being broken, and to use an optimization procedure to guide the testing towards falsification. The efficiency of the falsification is affected by the objective function used to evaluate the test results; different objective functions are differently efficient for different types of problems. However, the efficiency of various objective functions is not easily determined beforehand. This paper evaluates the efficiency of using multiple objective functions in the falsification process. The hypothesis is that this will, in general, be more efficient, meaning that it falsifies a system in fewer iterations, than just applying a single objective function to a specific problem. Two objective functions are evaluated, Max, Additive, on a set of benchmark problems. The evaluation shows that using multiple objective functions can reduce the number of iterations necessary to falsify a property.
|
|
| 8. |
- Ramezani, Zahra, 1988, et al.
(författare)
-
On Input Generators for Cyber-Physical Systems Falsification
- 2024
-
Ingår i: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. - 1937-4151 .- 0278-0070. ; 43:4, s. 1274-1287
-
Tidskriftsartikel (refereegranskat)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.
|
|
| 9. |
- Ramezani, Zahra, 1988
(författare)
-
On Optimization-Based Falsification of Cyber-Physical Systems
- 2022
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- In what is commonly referred to as cyber-physical systems (CPSs), computational and physical resources are closely interconnected. An example is the closed-loop behavior of perception, planning, and control algorithms, executing on a computer and interacting with a physical environment. Many CPSs are safety-critical, and it is thus important to guarantee that they behave according to given specifications that define the correct behavior. CPS models typically include differential equations, state machines, and code written in general-purpose programming languages. This heterogeneity makes it generally not feasible to use analytical methods to evaluate the system’s correctness. Instead, model-based testing of a simulation of the system is more viable. Optimization-based falsification is an approach to, using a simulation model, automatically check for the existence of input signals that make the CPS violate given specifications. Quantitative semantics estimate how far the specification is from being violated for a given scenario. The decision variables in the optimization problems are parameters that determine the type and shape of generated input signals. This thesis contributes to the increased efficiency of optimization-based falsification in four ways. (i) A method for using multiple quantitative semantics during optimization-based falsification. (ii) A direct search approach, called line-search falsification that prioritizes extreme values, which are known to often falsify specifications, and has a good balance between exploration and exploitation of the parameter space. (iii) An adaptation of Bayesian optimization that allows for injecting prior knowledge and uses a special acquisition function for finding falsifying points rather than the global minima. (iv) An investigation of different input signal parameterizations and their coverability of the space and time and frequency domains. The proposed methods have been implemented and evaluated on standard falsification benchmark problems. Based on these empirical studies, we show the efficiency of the proposed methods. Taken together, the proposed methods are important contributions to the falsification of CPSs and in enabling a more efficient falsification process.
|
|
| 10. |
- Ramezani, Zahra, 1988, et al.
(författare)
-
Temporal Logic Falsification of Cyber-Physical Systems using Input Pulse Generators
- 2021
-
Ingår i: EPiC Series in Computing. - : EasyChair. - 2398-7340. ; 80, s. 195-202
-
Konferensbidrag (refereegranskat)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.
|
|
