Falsification is a search-based testing technique based on hill climbing for CPS quality assurance, which aims to find a time-variant input signal u violating a formal specification describing the desired behavior. As illustrated by the figure below, the AI-enabled CPS represented by M^c takes input signal u and produces output signal M^c(u), which can be regarded as a black-box. Further, the system consists of an AI controller C and a physical system (Plant). The Plant is a system whose dynamics are given by a black-box function M, while AI-controller C with the inputs y(t) and u(t) outputs a control command c(t). Given a temporal specification φ, usually in the form of Signal Temporal Logic (STL) [1], falsification aims to hunt for a temporal signal u to the system that violates φ.

For this propose, Donzé [2] presents a quantitative robustness semantics of temporal formulas. Robust semantics extends the classical boolean satisfaction relation in the following sense: given a specification φ and an input signal u, it tells not only whether φ is satisfied or violated, but also how robustly the formula is satisfied or violated. Falsification is usually cast as an optimization approach that generates input signals with the aim of minimizing robustness. The search process terminates when an input signal with negative robustness is found, which means violate φ.

Falsification Tools. Up to the present, different optimization-based falsification methods have been proposed, and some well-known established tools (e.g., Breach [3] and S-TaLiRo [4] ) have also been developed. In RQ2, we select Global Nelder-Mead (GNM) and CMAES for Breach, and Simulated Annealing (SA) and stochastic optimization with adaptive restart (SOAR) for S-TaLiRo. Note that, although Breach and S-TaLiRo are based on the basic falsification algorithm, they have integrated different back-end optimization solvers to better achieve the search-based testing of CPS. In RQ2, we will call these four algorithms in abbreviated form for simplicity, namely, GNM-BR, CMAES-BR, SA-ST and SOAR-ST.

Experiment setup. Due to the randomness of falsification algorithms, we repeat each configuration for 30 times with an upper limit of 300 simulations each time. A corresponding falsification rate FR = # successful trials/ # total trials will be obtained. The time and #sim in the table below are the average time and simulation numbers of the successful trials.

To visually view the effectiveness of different falsification tools, we use histogram to present the abilities of different falsification algorithms for specific cases. For ACC-DDPG, both GNM-BR and SA-ST find one counterexample, compared with CMAES-BR and SOAR-ST. This also reflects the performance of ACC-DDPG controller to a certain extent. For ACC-TD3, GNM-BR and CMAES-BR completely outperform SA-ST and SOAR-ST. As for ACC-SAC and ACC-T, only CMAES-BR has slightly better performance.

For LKA, only LKA-DDPG cannot be falsified by these four algorithms. For four other CPS, there is no obvious difference on the effectiveness of these falsifiaiotn algorithms.

All of them cannot falsify CSTR-DDPG, CSTR-PPO and CSTR-TD3. This proves the performance of DRL-controllers to a certain extent. For CSTR-T, only GNM-BR does not achieve 100% FR.

The results of AFC clearly present the effectiveness of four falsification algorithms.

1. For AFC-DDPG, none of these four algorithms can find the input signal that violates the hard safety S1.

2. For AFC-PPO, only GNM-BR achieves a 100% falsification rate and CMAES-BR succeeds 10 times. Instead, SA-ST and SOAR-ST fails to seek an input signal that violates the hard safety S1.

3. The result of AFC-A2C is similar to AFC-PPO.

4. As for AFC-T, GNM-BR and CMAES-BR are inferior to two other algorithms.

For all SC systems with DRL controllers, the performance of four algorithms is completely consistent. However, The falsification rate of four algorithms achieve 100%. This is also shows that DRL controllers perform better than traditional PID controller from the side.

Summary.

1. Although falsification is the state-of-the-art validation method. However, it sometimes will fail to find counterexamples on AI-enabled CPS.

2. Different algorithms have distinct performance on the same AI-enabled CPS.

3. DRL-based controllers have more powerful and safer performance, compared with traditional controller, such as WTK. However, there are also some exceptions like APV.

Discussion.

1. The performance of these four falsification algorithms has been evaluated and analyzed in detail. For the failed falsification cases, on the one hand, it partly depends on the concrete search algorithm; on the other hand, the trajectory of AI-enabled controllers with more local minimum or non-differentiable points makes the search process more difficult. The above results prove the famous no free lunch theorem in optimization, and also motivates us to develop more effective algorithms to handle these emerging AI-enabled CPS.

2. From another perspective, new DRL training methods and strategies are urgently needed to better train the controllers that perform some complex control tasks.

1. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)

2. Donzé A, Maler O. Robust satisfaction of temporal logic over real-valued signals. International Conference on Formal Modeling and Analysis of Timed Systems. Springer, Berlin, Heidelberg, 2010: 92-106.

3. Donzé, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)

4. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-taLiRo: A tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011)