Hierarchical Optimization for Hybrid System Falsi cation

I would like to express my deepest gratitude to my supervisor, Ichiro Hasuo, for his continuous supervisions and support to me. I would like to thank Gidon Ernst and Sean Sedwards for their guidance on my current research topic.

Cyber-Physical Systems

CPS is usually referred to in the abstract sense to hybrid systems: they combine discrete and continuous dynamics together in a single system. The roles computer software plays are usually control and monitoring: they monitor the behavior of mechanical systems, and send commands to control them based on a set of business logic rules.

Quality Assurance of CPS

A Usage Scenario: an Automotive System

However, this is not a trivial problem for the engineer, since the car is made up of so many blocks that operate according to complicated dynamics. Here comes the problem—is there a good way to determine whether the car satisfies that property.

Verification

The negation of the system specification in the form of temporal logics, which represent the unexpected situation, can be transformed into another automaton. However, given the general nature of the model of hybrid automatons, the time divergence of a run is not always guaranteed.

Testing

Hybrid systems are expressed in the form of hybrid programs [10, 11] and tools can automatically prove whether the system satisfies a given property in DL. It adds infinitesimal notation to the traditional programming language, which allows it to express continuous dynamics and thus describes the implementation of hybrid systems.

Optimization-Based Falsification

• Quantitative STL Robustness
• Stochastic Optimization-Based Falsification
• Usage Scenario of Falsification
• Current Status of Falsification in Academia and Industry

Specification System specifications (as presented in §1.2) can be used to formalize criteria, such as security concerns, that the system must satisfy. So far we have gone through the workflow of the optimization-based forging technique, as illustrated in Fig 1.6.

Motivation: Existing Problems and Related Works

Exploration and Exploitation

In [62], the authors apply the famous colony optimization to forgery, where the search takes a small probability to start a new exploration. In [71], the authors exploit the causality between the subformulas and the global formula of the specification to speed up the search.

Robust Semantics Definition

In [26], the authors study the application of reinforcement learning to forgery, where they discretize the input signal as a sequence of actions and search in an incremental way. Reinforcement learning is also applied in the context of testing autonomous vehicles [74] for the detection of dangerous scenarios, which goes through a similar workflow with spoofing.

Input Constraints

Intuitively, if the subformulas refer to different signals spanning different scales, then the comparison becomes unfair because one can always beat the other. In this part, they explicitly declare the input and output signals by manually introducing a bias in the comparison.

A Hierarchical Optimization Framework

It first decomposes the problem into a set of subproblems, and then uses a hierarchical methodology: the upper layer makes a decision about choosing one child problem as the next step to proceed, based on the information obtained from the lower layer come; the lower layer performs numerical optimization on the subproblem represented by the upper layer, and it provides feedback to the upper layer. One feature of this framework is the interaction between the two layers: the upper layer makes high-level decisions and advises the lower layer; the lower layer performs concrete numerical evaluation and provides feedback to the upper layer to facilitate the future decisions.

Organization

System Models

This derives the difference between discrete systems and hybrid systems: in discrete systems all state transitions are “jumps”, while in hybrid systems physical components are as continuous.

Robust Semantics for STL

It follows from the definition that the robustness for the ultimate modality is given by Jw,^[a,b](x >0)K= Ã. Our choice of spatial robustness in this paper is for the sake of simplicity, and is therefore not essential.

Hill Climbing-Guided Falsification

It follows from the definition that the robustness for the eventual modality is given by Jw,^[a,b](x >0)K= Ã. The above robustness concept taken from [32] is therefore spatial. It is specialized in searching for local optimum but unable to jump out of it to search for global optimum.

Evaluation Metrics of Falsification Algorithms

Cooperation between research and exploitation is thus very important, especially in the case of a limited budget, for example in counterfeiting. In this chapter, we tackle the problem of balancing exploration and exploitation during search using a technique based on Monte Carlo Tree Search (MCTS).

Exploiting Time Causality via Time Staging

Time-Staging Approach

It then calls the Hill-Climb-Falsify function K times; on each Hill-Climb-Falsify loop, it finds the best signal segment0 and connects it to you. This creates a new problem, ie. the "local optimum" trap arising from temporal staging.

Falsification with Monte Carlo Tree Search

Monte Carlo Tree Search

For example, in the game of Go, reward is correlated with the outcome of the game, i.e. win or lose. In case of "win", we update the counter of the reward by 1; otherwise it will be 0.

The Basic Two-Layered Algorithm

Initially, the tree T is root-only (line 3), and in each iteration—called MCTS sampling—the call to MCTSSample on line 10 adds one new node to T. In the rest of the Main function, the second hill-climbing optimization is performed for adulteration, where our samples according to→−.

The Two-Layered Algorithm with Progressive Widening

Experimental Evaluation

Experiment Setup

The basic requirement for AFC is to keep the air-to-fuel ratio AF close to the reference AFref. The goal is to find spikes where the ratio has decreased by a fraction 0.01 of the reference value for at least 0 seconds during.

Performance Evaluation

M_b (MCTS budget) is the maximum number of visits to the root of the MCTS search tree (i.e. the maximum number of tree nodes). However, it increases the adulteration rate with GNM and SA, for the same reasons as before.

Evaluation of Parameter Choices

Conversely, South Africa is heavily dependent on exploration and retains only a single good track found to date, limiting its exploitation. However, progressive broadening has a positive effect on the success rate and decay time for S2 and S5.

Discussion

In this chapter, we tackle the scaling problem arising from the definition of STL robust semantics for Boolean connections (conjunctive and disjunctive) in the existing falsification framework. We first explain the problem caused by the improper definition of robust semantics for Boolean connections in §4.1, and then present the proposed approach in §4.2.

Motivation: the Scale Problem

In this case, when we compare the robustness values ​​at a point where both are positive, one is likely to be greater in terms of speed, e.g. in the interval [25,30] of sample1 or the interval [20,30] of sample2. In [75], the authors propose a method that explicitly declares input signals and output signals, thus manually introducing a bias in the comparison of robustness values ​​of subformulas concerning different signals.

Multi-Armed Bandit-Based Falsification Algorithm

• Conjunctive and Disjunctive Safety Properties
• The Multi-Armed Bandit (MAB) Problem
• Our MAB-Guided Algorithm I: Conjunctive Safety Proper- tiesties
• Our MAB-Guided Algorithm II: Disjunctive Safety Proper- ties

Multi-Armed Bandits for Boolean Connections in STL Algorithm 4.3 Our MAB-Guided Algorithm I: Conjunctive Safety Properties. The numerator max-rb(i,k−1) −last-rb(i,k−1) then represents how much robustness we have reduced by hill climbing so far - hence the name "hill climbing gain." The denominator max-rb(i,k−1) is there for normalization.

Experimental Evaluation

Experiment Setup

The new Line 7' measures the quality of the proposed input signal in a way limited to the regionSk in which the other formula has already been falsified. We built the benchmark setBbench, as shown in Table 4.1a, which lists the name of the model and its specifications (ID and formula).

Evaluation

The observation is confirmed by the Wilcoxon test over SR: the null hypothesis is rejected with p-value=1.808e-09 and the alternative hypothesis is accepted with p-value=1. Instead, the null hypothesis that there is no difference with respect to time cannot be rejected with p-value=0.3294.

A Comparison to a Normalization-Based Approach

We can see that the final robustness comes from the robustness to subformularpm <4780.

Motivation and Problem Definition

Problem Definition

We simply use the STL to express the constraints, because ψ is a temporal property that the input signal is assumed to satisfy. Note that these two formalisms have equivalent expressiveness provided we use piecewise constants as input signals, as we show in §5.6.1, where we explain how we can transform one into the other.

Penalty-Based Approaches

Constraint Embedding Approach

Lexicographic Method Approach

Also in this case, negative values ​​of robustness mean that the goal has been achieved (i.e. the specification has been falsified). Note that in the definition of GCFfal we do not apply the ceiling operator to the robustness evaluation of the specificationφ(i.e. f2).

Discussion: Weaknesses of the Penalty-Based Approaches

In fact, removing the ceiling avoids the quantization effect that is generally adversarial to hillclimb search. The proof comes directly from the definitions of GCFfal, T1 and T2 and the robustness definition of STL.

Problem Setting and Overview of the Search Space Transformation-Based Approach

Search Space Transformation-Based Approach

We also define the fitness function of the points of the search spaceΞbased on the fitness of the input spaceΩψ. To guarantee this, hill climbing in the search spaceΞ must obtain a faithful representation of the fitness landscape of the input spaceΩψ.

Proportional Transformation

SAAAB+XicdVDLSgMxFL1TX7W+Rl26CRahgpSZUtCNUHTjsqJ9QDsOmTTThmYeJJnSMxMvHcdVDLhs dzJpVlvRu5peWV1bX8emFjc2t7x9zda8ooEYQ2SMQj0fawpJyFtKGY4rQdC4oDj9OWN7zM/NaICsmi8FZNYuoEuB8ynxGstOSa5s2djc5RaezaV3V3JmV3VQV1Djc5RaezaV3VQV1DJ2005V3VQV1DJ2005V3V3VQV105 fur2IJAENFeFYyo5txcpJsVCMcDotdBNJY0yGuE87moY4oNJJZ5dP0ZFWesiPhK5QoZn6dSPFgZSTwNOTAVYD+dPLxL+8TqL8MydlYZwoGPqMMFL5QFh3 A6roEP4/Cn6nzQrZdsq29fVYu1iEUceDuAQSmDDKdTgCurQAAIjuIdHeDJS48F4Nl7mozljsbMP32C8fgAmipFkAAAB+XicdVDLSgMxFL1TX7W+Rl26CRahgpSZUtCNUHTjsqJ9QDsOmTTThmYeJJnSMvRP3LhQxK1/4s6/MdNW8Hngcg/n3Etuj8FXV000000/n3Etuj8VXv1vd 8ooEYQ2SMQj0fawpJyFtKGY4rQdC4oDj9OWN7zM/NaICsmi8FZNYuoEuB8ynxGstOSa5s2djc5RaezaJ2jsVo5ds2iVq1YG9JvY5Vm3irBAY5JpJpJpJpJpJpJcFcf Y0yGuE87moY4oNJJZ5dP0ZFWesiPhK5QoZn6dSPFgZSTwNOTAVYD+dPLxL+8TqL8MydlYZwoGpL5Q37CkYpQFgPqMUGJ4hNNMBFM34rIAEPzQ1qVceDu66 uAQSmDDKdTgCurQAAIjuIdHeDJS48F4Nl7mozljsbMP32C8fgAmipFkAAAB+XicdVDLSgMxFL1TX7W+Rl26CRahgpSZUtCNUHTjsqJ9QDsOmTTThmYeJJnSMvRP3LhQxK1/4Wn3HpeJpJplmgd WV1bX8emFjc2t7x9zda8ooEYQ2SMQj0fawpJyFtKGY4rQdC4oDj9OWN7zM/NaICsmi8FZNYuoEuB8ynxGstOSa5s2djc5RaezaJ2jsVo5GY4rQdC4oDj9OWN7zM/NaICsmi8FZNYuoEuB8ynxGstOSa5s2djc5RaezaJ2jsVo5G92iVFYJA 5txcpJsVCMcDotdBNJY0yGuE87moY4oNJJZ5dP0ZFWesiPhK5QoZn6dSPFgZSTwNOTAVYD+dPLxL+8TqL8MydlYZwoGpL5Q37CkYpGJMQFhnFr6MBt4MF4NF4MF4NFNF4MF4NF4MQNFQNF4MbAn QrZdsq29fVYu1iEUceDuAQSmDDKdTgCurQAAIjuIdHeDJS48F4Nl7mozljsbMP32C8fgAmipFk 1= (x1, x2). lt;latexit sha1_base64="EbmPdffY9mP/DplTFisIpE9hYgY=">AAAB+XicdVDLSgMxFL1TX7W+Rl26CRahgpSZUtCNUHTjsqJ9QDsOmTTThmYeJL4WsMxRp3/Aaaaab+XicdVDLSgMxFL1TX7W+Rl26CRahgpSZUtCNUHTjsqJ9QDsOmTTThmYeJL4WsMxRp tujhdzJpVlvRu5peWV1bX8emFjc2t7x9zda8ooEYQ2SMQj0fawpJyFtKGY4rQdC4oDj9OWN7zM/NaICsmi8FZNYuoEuB8ynxGstOSa5s1dBZMExaj0GB000+1dBZMExajv00 u+dXsRSQIaKsKxlB3bipWTYqEY4XRa6CaSxpgMcZ92NA1xQKWTzi6foiOt9JAfCV2hQjP160aKAykngacnA6wG8qeXiX95nUT5Z07KwjhECZ92NA1xQKWTzi6foiOt9JAfCV2hQjP160aKAykngacnA6wG8qeXiX95nUT5Z07KwjhECZ92NA1xQKWTz KB1WQYfw+VP0P2lWyrZVtq+rxdrFIo48HMAhlMCGU6jBFdShAQRGcA+P8GSkxoPxbLzMR3PGYmcfvsF4/QAoIJFlAAAB+XicdVDLSgMxFL1TX7W+Rl26CRahgpSZUtHmDjQmJQNJT QxK1/4s6/MdNW8Hngcg/n3EtujhdzJpVlvRu5peWV1bX8emFjc2t7x9zda8ooEYQ2SMQj0fawpJyFtKGY4rQdC4oDj9OWN7zM/ NaICsmi8FZNYuoEuB8ynxGstOSa5s1dBZ2j0titnKCxax+7ZtEqV60M6Dexy7NuFWGBumu+dXsRSQIaKsKxlB3bipWTYqEY4XRa6CaSxpgMcZKW2KafqV601FMcZKW200JF ykngacnA6wG8qeXiX95nUT5Z07KwjhRNCTzh/yEIxWhLAbUY4ISxSeaYCKYvhWRARaYKB1WQYfw+VP0P2lWyrZVtq+rxdrFIo48HMAhlMCGDrFIo48HMAhlMCGDrFIo48HMAhlMCGDShMkRXRBFShMXPXRXBFHLMXPXRXBF8MHPXRXBFRXHPXRXHBFQMHPXRXBFS cfvsF4/QAoIJFl. lt;latexit sha1_base64="LikKNUqT8dPAavvLZwaoeMS7Zcc=">AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQMxHvMDQ5/gQMxvHyh5 w6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpodcRfbfq1bw19DUFQ1bw19UC sxyKlGwSSfVnqZ4SllYzrkXUsVjbkJ8vmpU3JmlQGJEm1LIZmrvydyGhsziUPbGVMcmWVvJv7ndTOMroNcqDRDrthiUZRJggmZ/U0GQnOGcmIJZVqNV0VRv0+VRV0+VRV0+VR+ +s1m+KOMpwAqdwDj5cQR3uoAFNYDCEZ3iFN0c6L86787FoLTnFzDH8gfP5AytFjbU=AAAB6nicbVBNS8NAEJ3Ur1q/oh69LBbBU0lE0GPRi8eK9gPaUDbbTbt0swm7E6GE/gQvHhTx6i/y5r9x2+agrQ8GHu/NMDMvTKUw6HnfTmltfWNzq7xd2dnd2z9wD49aJsk0402WyER3Qmq4FIo3UaDknVRzGoeSt8Px7cxvP3FtRKIecZLyIKZDJSLBKFrpodcRfbfq1bw5yCrxC1KFAo2+ +9UbJCyLuUImqTFd30sxyKlGwSSfVnqZ4SllYzrkXUsVjbkJ8vmpU3JmlQGJEm1LIZmrvydyGhsziUPbGVMcmWVvJv7ndTOMroNcqDRDrthiUZRJGQZwqmZUCMZRJGQbqmV0U/ NgR/+eVV0rqo+V7Nv7+s1m+KOMpwAqdwDj5cQR3uoAFNYDCEZ3iFN0c6L86787FoLTnFzDH8gfP5AytFjbU=.

Falsification Based on the Proportional Transfor- mationmation

Method 1: Fixed-Priority

Method 2: All-Priorities

Given two priorities S1 and S2, if they differ only in the relative order of independent variables, they are equivalent. Note that even if two priorities are not equivalent, a point can still be assigned to the same point under both priorities: therefore, on Line 6, duplicate points are removed.

Method 3: MAB-Priority

The reward of a priorityS is based on the minimum robustness value observed when using S to map the sampled point (i.e., playing that arm). The exploration score is a value that is negatively correlated with the number of attempts of the branch of priority Sz.

Experimental Evaluation

Experiment Setup

Then we determine the input constraints Rψmax by multiplying the maximum value of the robustness values ​​obtained by a reasonable factor. The model is composed of 11 subsystems, including a neural network-based controller, and 104 blocks in total.

Evaluation

These two layers work closely together to improve search efficiency and effectiveness. It forms such a framework: MAB algorithms on the upper layer choose one of the machines according to their rewards;.

Discussion: Integration of the Techniques

If their application has no input constraints to deal with, then the sample and input signal in Fig. Therefore, our work provides practitioners with a more powerful forgery tool than modern technology.

Future works

Fourth IEEE International Conference on Software Testing, Verification and Validation, ICST 2012, Berlin, Germany, 21-25 March 2011, workshop proceedings, pages 153-163. In Proceedings of the 17th International Conference on Tools and Algorithms for Systems Construction and Analysis: Part of the Joint European Conferences on Software Theory and Practice, TACAS’11/ETAPS’11, pages 254–257, Berlin, Heidelberg, 2011.

MATLAB Source Code for the Usage Scenario

Raw Experimental Results for Table 4.2