Title: Counterexample generation in CPS model checking based on ARSG algorithm

Authors: Mingguang Hu; Zining Cao; Fujun Wang; Weiwei Lu

Addresses: College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China ' College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China; Science and Technology on Electro-optic Control Laboratory, Luoyang, China; Key Laboratory of Safety-Critical Software, Ministry of Industry and Information Technology, Nanjing, China; MIIT Key Laboratory of Pattern Analysis and Machine Intelligence, Nanjing University of Aeronautics and Astronautics, Nanjing, China ' College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China ' Science and Technology on Electro-optic Control Laboratory, Luoyang, China

Abstract: With the rapid development of software and physical devices, cyber-physical systems (CPS) are widely adopted in many application areas. Due to the increasing complexities of these systems, it is difficult to detect defects in CPS models. Counterexample generation in CPS model checking is a good choice as it is able to find defects in CPS models efficiently and can provide meaningful diagnostic feedback to facilitate debugging. In many studies, robustness-guided counterexample generation of CPS is investigated by various optimisation methods, which falsify the given properties of a CPS. In this paper, we combine genetic algorithm (GA) with acceptance-rejection technique based on the neighbourhood of the input sequence space, and propose a novel algorithm which is called ARSG algorithm. The idea of this algorithm is similar to 'exploration-exploitation' in reinforcement learning. Finally, the new algorithm is compared with the cross-entropy algorithm and the genetic algorithm under different parameters, and the performance of the new algorithm is better than the other two algorithms.

Keywords: cyber-physical systems; CPS; signal temporal logic; counterexample generation; acceptance-rejection technique; genetic algorithm.

DOI: 10.1504/IJCSE.2021.115658

International Journal of Computational Science and Engineering, 2021 Vol.24 No.3, pp.312 - 321

Received: 19 Mar 2020
Accepted: 08 Dec 2020
Published online: 15 Jun 2021 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article