Computer Science

Computer Science ›› 2025, Vol. 52 ›› Issue (12): 24-31.doi: 10.11896/jsjkx.241100062

• Computer Software & Architecture • Previous Articles     Next Articles

SCADE Model Checking Based on Implicit Predicate Abstraction and Property-directedReachability

ZHANG Cong1, CHEN Zhe1,2, WANG Huijie1, WEI Yiyang1   

  1. 1 College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China
    2 Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 211106, China
  • Received:2024-11-11 Revised:2025-02-12 Online:2025-12-15 Published:2025-12-09
  • About author:ZHANG Cong,born in 1999,postgra-duate.His main research interests include model checking and software safety.
    CHEN Zhe,born in 1981,professor,is a senior member of CCF(No.22234S).His main research interests include formal methods,software verification and software engineering.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China(62172217) and Joint Research Funds of National Natural Science Foundation of China and Civil Aviation Administration of China(U1533130).

PDF (PC)

57

Abstract: SCADE is widely used in critical industries related to life safety,such as aerospace,nuclear power plants,rail transit,and medical equipment.Applying model checking to these safety critical areas can effectively ensure the safety of the system.At present,there is relatively little research on SCADE model checking.Most studies are based on program translation and use other simpler language model checking tools to complete verification.However,few tools that have implemented the entire process of model checking for SCADE programs have low verification efficiency.This paper proposes a model checking algorithm based on implicit predicate abstraction and property-directed reachability(IAPDR),which is parallelly integrated into existing model che-cking tools(PSMC) for SCADE programs.The tool implements the entire process of analysis,modeling,and model checking for SCADE programs.In addition,the correctness of the proposed algorithm is theoretically proven,and the effectiveness and performance of the expanded tool(PSMCWI) are evaluated through experiments.Compared with traditional BMC,K-Induction,and CEGAR algorithms,IAPDR has the highest verification success coverage and the lowest total verification time on the benchmarks.Compared with the native PSMC tool,PSMCWI can verify 139 more SCADE programs on the benchmarks,with a 15.1% increase in successful verification coverage and a 43% reduction in total verification time.The results of the comparative experiment with JKind show that IAPDR can correctly do model checking on SCADE programs.Compared with the method of translating SCADE models into Lustre models and using JKind to do model checking on Lustre models to achieve model checking on SCADE programs,PSMCWI has higher efficiency.

Key words: SCADE, Model checking, States space, Predicate abstraction, Property-directed reachability, Interpolation

CLC Number: 

  • TP311
[1]COLAÇO J L,PAGANO B,POUZET M.SCADE 6:A formallanguage for embedded critical software development[C]//2017 International Symposium on Theoretical Aspects of Software Engineering(TASE).IEEE,2017:1-11.
[2]RAN D,CHEN Z,SUN Y,et al.SCADE model checking based on program translation [J].Computer Science,2021,48(12):125-130.
[3]GACEK A,BACKES J,WHALEN M,et al.TheJKind model checker[C]//International Conference on Computer Aided Verification.Cham:Springer,2018:20-27.
[4]WANG H,YANG Z,ZHOU Y,et al.AGVTS:Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models[C]//International Symposium on Formal Methods.Cham:Springer,2024:338-355.
[5]CAVADA R,CIMATTI A,DORIGATTI M,et al.The nuXmv symbolic model checker[C]//International Conference on Computer Aided Verification.Cham:Springer,2014:334-342.
[6]LI T F,SUN J F,LYU X J,et al.Formal verification of synchronous reactive model for SMT based regional controller [J].Journal of Software,2023,34(7):3080-3098.
[7]BARRETT C,TINELLI C.Satisfiability modulo theories[M]//HandBook of Model Checking.Cham:Springer,2018:305-343.
[8]BASOLD H,GUNTHER H,HUHN M,et al.An open alterna-tive for SMT-based verification of SCADE models[C]//International Workshop on Formal Methods for Industrial Critical Systems.Cham:Springer,2014:124-139.
[9]BJESSE P,CLAESSEN K.SAT-based verification without state space traversal[C]//International Conference on Formal Me-thods in Computer-Aided Design.Berlin:Springer,2000:409-426.
[10]DE MOURA L,RUEϐ H,SOREA M.Bounded model checking and induction:From refutation to verification[C]//International Conference on Computer Aided Verification.Berlin:Springer,2003:14-26.
[11]FANG Y Y,ZHANG C.SCADE model checking based on multi engine parallel collaboration[J].Computer Technology and Development,2023,33(11):86-90.
[12]CIMATTI A,GRIGGIO A,MOVER S,et al.IC3 modulo theories via implicit predicate abstraction[C]//International Confe-rence on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2014:46-61.
[13]BRADLEY A R.SAT-based model checking without unrolling[C]//International Workshop on Verification,Model Checking,and Abstract Interpretation.Berlin:Springer,2011:70-87.
[14]YU Z Q,ZHANG X Y,LI J W,et al.Approximate reachability analysis based on unsatisfiable kernels [J].Journal of Software,2023,34(8):3467-3484.
[15]LI J,ZHU S,ZHANG Y,et al.Safety model checking with complementary approximations[C]//2017 IEEE/ACM International Conference on Computer-Aided Design(ICCAD).IEEE,2017:95-100.
[16]ZHANG X,XIAO S,XIA Y,et al.Accelerate safety model checking based on complementary approximate reachability[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2023,42(9):3105-3117.
[17]MCMILLAN K L.Interpolation and SAT-based model checking[C]//International Conference on Computer Aided Verification.Berlin:Springer,2003:1-13.
[18]CRAIG W.Linear reasoning:A new form of the Herbrand-Gentzen theorem[J].Symbolic Logic,1957,22(3):250-268.
[19]EEN N,MISHCHENKO A,BRAYTON R.Efficient implementation of property directed reachability[C]//2011 Formal Me-thods in Computer-Aided Design(FMCAD).IEEE,2011:125-134.
[20]DE MOURA L,BJORNER N.Z3:An efficient SMT solver[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2008:337-340.
[21]CIMATTI A,GRIGGIO A,SCHAAFSMA B J,et al.The math-sat5 smt solver[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2013:93-107.
[22]COK D R.The smt-libv2 language and tools:A tutorial[J].Language C,2011:14-55.
[1] CHEN Jun, ZHOU Qiang, BAO Lei, TAO Qing. Linear Interpolation Method for Adversarial Attack [J]. Computer Science, 2025, 52(8): 403-410.
[2] ZHANG Haoran, WANG Guiling. Multi-target Trajectory Generation Method Based on Motion Features [J]. Computer Science, 2025, 52(8): 154-161.
[3] CHEN Zhangyuan, CHEN Ling, LIU Wei, LI Bin. Method for Selecting Observers Based on Doubly Resolving Set in Independent Cascade Model [J]. Computer Science, 2025, 52(4): 280-290.
[4] HU Peng, XIA Xiaohua, ZHONG Yuquan. Road Crack Detection Method for Embedded Applications [J]. Computer Science, 2025, 52(12): 175-188.
[5] WANG Qian, HE Lang, WANG Zhanqing, HUANG Kun. Road Extraction Algorithm for Remote Sensing Images Based on Improved DeepLabv3+ [J]. Computer Science, 2024, 51(8): 168-175.
[6] SHAO Wenxin, YANG Zhibin, LI Wei, ZHOU Yong. Natural Language Requirements Based Approach for Automatic Test Cases Generation of SCADE Models [J]. Computer Science, 2024, 51(7): 29-39.
[7] DENG Ziwei, CHEN Ling, LIU Wei. Continuous Influence Maximization Under Independent Cascade Propagation Model [J]. Computer Science, 2024, 51(6): 161-171.
[8] LI Yu, YANG Xiangli, ZHANG Le, LIANG Yalin, GAO Xian, YANG Jianxi. Combined Road Segmentation and Contour Extraction for Remote Sensing Images Based on Cascaded U-Net [J]. Computer Science, 2024, 51(3): 174-182.
[9] WANG Yuchen, GAO Chao, WANG Zhen. Survey of Inferring Information Diffusion Networks [J]. Computer Science, 2024, 51(1): 99-112.
[10] BAI Mingli, WANG Mingwen. Fabric Defect Detection Algorithm Based on Improved Cascade R-CNN [J]. Computer Science, 2023, 50(6A): 220300224-6.
[11] ZHENG Hong, QIAN Shihui, LIU Zerun, DU Wen. Formal Verification of Supply Chain Contract Based on Coloured Petri Nets [J]. Computer Science, 2023, 50(6A): 220300220-7.
[12] ZHANG Zelun, YANG Zhibin, LI Xiaojie, ZHOU Yong, LI Wei. Machine Learning Based Environment Assumption Automatic Generation for Compositional Verification of SCADE Models [J]. Computer Science, 2023, 50(6): 297-306.
[13] LI Yuqiang, LI Huan, LIU Chun. Improved Fast Image Translation Model Based on Spatial Correlation and Feature Level Interpolation [J]. Computer Science, 2023, 50(12): 156-165.
[14] YANG Liu, FAN Hongyu, LI Dongfang, HE Fei. IC3 Hardware Verification Algorithm Based on Variable Hiding Abstraction [J]. Computer Science, 2023, 50(11A): 230200112-6.
[15] CHEN Bonian, HAN Yutong, HE Tao, LIU Bin, ZHANG Jianxin. Cascade Dynamic Attention U-Net Based Brain Tumor Segmentation [J]. Computer Science, 2023, 50(11A): 221100180-7.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.