A Novel GAPG Approach to Automatic Property Generation for Formal Verification: The GAN Perspective

被引:16
作者
Gao, Honghao [1 ]
Dai, Baobin [1 ]
Miao, Huaikou [1 ]
Yang, Xiaoxian [2 ]
Barroso, Ramon J. Duran [3 ]
Walayat, Hussain [4 ]
机构
[1] Shanghai Univ, Sch Comp Engn & Sci, Shanghai 200444, Peoples R China
[2] Shanghai Polytech Univ, Sch Comp & Informat Engn, Shanghai 201209, Peoples R China
[3] Univ Valladolid, Fac Telecommun Engn, Valladolid 47002, Spain
[4] Univ Technol Sydney, Fac Engn & IT, Sydney, NSW 2007, Australia
基金
中国国家自然科学基金;
关键词
Model checking; verification property; generative adversarial network (GAN); automatic property generation; computational tree logic; correctness and reliability; ADVERSARIAL NETWORKS;
D O I
10.1145/3517154
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Formal methods have been widely used to support software testing to guarantee correctness and reliability. For example, model checking technology attempts to ensure that the verification property of a specific formal model is satisfactory for discovering bugs or abnormal behavior from the perspective of temporal logic. However, because automatic approaches are lacking, a software developer/tester must manually specify verification properties. A generative adversarial network (GAN) learns features from input training data and outputs new data with similar or coincident features. GANs have been successfully used in the image processing and text processing fields and achieved interesting and automatic results. Inspired by the power of GANs, in this article, we propose a GAN-based automatic property generation (GAPG) approach to generate verification properties supporting model checking. First, the verification properties in the form of computational tree logic (CTL) are encoded and used as input to the GAN. Second, we introduce regular expressions as grammar rules to check the correctness of the generated properties. These rules work to detect and filter meaningless properties that occur because the GAN learning process is uncontrollable and may generate unsuitable properties in real applications. Third, the learning network is further trained by using labeled information associated with the input properties. These are intended to guide the training process to generate additional new properties, particularly those that map to corresponding formal models. Finally, a series of comprehensive experiments demonstrate that the proposed GAPG method can obtain new verification properties from two aspects: (1) using only CTL formulas and (2) using CTL formulas combined with Kripke structures.
引用
收藏
页数:22
相关论文
共 42 条
[41]  
Yu LT, 2017, AAAI CONF ARTIF INTE, P2852
[42]   DeepRoad: GAN-Based Metamorphic Testing and Input Validation Framework for Autonomous Driving Systems [J].
Zhang, Mengshi ;
Zhang, Yuqun ;
Zhang, Lingming ;
Liu, Cong ;
Khurshid, Sarfraz .
PROCEEDINGS OF THE 2018 33RD IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMTED SOFTWARE ENGINEERING (ASE' 18), 2018, :132-142