计算机科学

计算机科学 ›› 2025, Vol. 52 ›› Issue (12): 24-31.doi: 10.11896/jsjkx.241100062

• 计算机软件&体系架构 • 上一篇    下一篇

基于隐式谓词抽象和属性导向可达的SCADE模型检测

张聪1, 陈哲1,2, 王慧杰1, 韦依洋1   

  1. 1 南京航空航天大学计算机科学与技术学院 南京 211106
    2 软件新技术与产业化协同创新中心 南京 211106
  • 收稿日期:2024-11-11 修回日期:2025-02-12 出版日期:2025-12-15 发布日期:2025-12-09
  • 通讯作者: 陈哲(zhechen@nuaa.edu.cn)
  • 作者简介:(1912460139@qq.com)
  • 基金资助:
    国家自然科学基金(62172217);国家自然科学基金委员会-中国民航局民航联合研究基金(U1533130)

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 Published:2025-12-15 Online: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)

56

摘要： SCADE被广泛应用于航空航天、核电站、轨道交通、医疗设备等关乎生命安全的关键行业。将模型检测应用于这些安全关键领域,能够有效地确保系统的安全。目前,针对SCADE模型检测的研究较少,多数研究基于程序转化,借助其他更简单的语言模型检测工具来完成验证,而少有的可实现对SCADE程序进行模型检测的全流程工具则验证效率较低。为此,提出了一种基于隐式谓词抽象和属性导向可达的模型检测算法(IAPDR),将其并行集成到现有的针对SCADE程序的模型检测工具(PSMC)上,该工具实现了SCADE程序的分析、建模和模型检测的全流程。此外,通过理论证明了所提出算法的正确性,通过实验评估了IAPDR算法以及扩展后的工具(PSMCWI)的效果和性能。与传统的BMC,K-Induction和CEGAR算法相比,IAPDR 算法在数据集上具有最高的验证成功覆盖率和最短的验证总耗时。与原生的PSMC工具相比,PSMCWI在数据集上能够多验证139个SCADE程序,验证成功覆盖率提升了15.1%,验证的总耗时减少了43%。与JKind的对比实验的结果表明,IAPDR算法能够正确地对SCADE程序进行模型检测,相比于将SCADE模型转化为Lustre模型后,用JKind对Lustre模型进行模型检测来实现对SCADE程序进行模型检测的方法,PSMCWI具有更高的效率。

关键词: SCADE, 模型检测, 状态空间, 谓词抽象, 属性导向可达, 插值

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

中图分类号: 

  • 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.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
地址：重庆市渝北区洪湖西路18号    邮编：401121  
电话：023-63500828（编辑部） 023-67039612（会议/专题） 023-67039623（财务/发票）
E-mail：jsjkx12@163.com
本系统由北京玛格泰克科技发展有限公司设计开发