基于不可满足核的近似逼近可达性分析
作者:
作者简介:

于忠祺(1997-),男,硕士生,主要研究领域为形式化验证,模型检测;李建文(1987-),男,博士,研究员,博士生导师,CCF专业会员,主要研究领域为形式化方法,软硬件安全;张小禹(1997-),男,博士生,CCF学生会员,主要研究领域为形式化方法,模型检测算法.

通讯作者:

李建文,E-mail:jwli@sei.ecnu.edu.cn

基金项目:

国家自然科学基金(62002118,U21B2015);上海市浦江人才计划(19511103602);上海市可信工业互联网软件协同创新中心(2021-2025)


UC-based Approximate Incremental Reachability
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [56]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    近年来,形式化验证技术受到了越来越多的关注,它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支,具有十分广阔的发展前景.研究并提出了一种新的模型检测技术,可以有效地对迁移系统进行模型检测,包括不安全性检测和证明安全性.与现有的模型检测算法不同,提出的基于不可满足核(unsatisfied core,UC)的近似逼近可达性分析(UC-based approximate incremental reachability,UAIR),主要利用不可满足核来求解一系列的候选安全不变式,直至生成最终的不变式,以此来实现安全性证明和不安全性检测(漏洞查找).在基于SAT求解器的符号模型检测中,使用由可满足性求解器得到的UC构造候选安全不变式,如果迁移系统本身是安全的,得到的初始不变式只是安全不变式的一个近似.然后,在检查安全性的同时,逐步改进候选安全不变式,直到找到一个真正的不变式,证明系统是安全的;如果系统是不安全的,该方法最终可以找到一个反例证明系统是不安全的.作为一种全新的方法,利用不可满足核进行安全性模型检测,取得了相当好的效果.众所周知,模型检测领域没有绝对最好的方法,尽管该方法在基准的可解数量上无法超越当前的成熟方法,例如IC3,CAR等,但是该方法可以解出3个其他方法都无法解出的案例,相信本方法可以作为模型检测工具集很有价值的补充.

    Abstract:

    In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in critical areas of safety. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. This work studies and proposes a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, the proposed method, unsatisfied core (UC)-based approximate incremental reachability (UAIR), mainly utilizes the unsatisfied core to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, the UC obtained by the satisfiability solver is used to construct candidate safety invariant, and if the transition system itself is safe, the initial invariant obtained is only an approximation of the safety invariant. Then, while checking the safety, the candidate safety invariant is gradually improved until a real invariant is found that proves the system is safe; if the system is unsafe, the proposed method can finally find a counterexample to prove the system is unsafe. As a brand new method, UCs are exploited for safety model checking and sound results are achieved. As it is all known, there is no absolute best method in the field of model checking, although the proposed method cannot surpass the current mature methods such as IC3, CAR, etc., the method in this paper can solve 3 cases that other mature methods are unable to solve, it is believed that this method can be a valuable addition to the model checking toolset.

    参考文献
    [1] Golnari A, Vizel Y, Malik S.Error-tolerant processors:Formal specification and verification.In:Proc.of the 2015 IEEE/ACM Int'l Conf.on Computer-Aided Design (ICCAD).IEEE, 2015.286-293.
    [2] Rozier KY.Linear temporal logic symbolic model checking.Computer Science Review, 2011, 5(2):163-203.
    [3] Baier C, Katoen JP.Principles of Model Checking.MIT Press, 2008.
    [4] Bernardini A, Ecker W, Schlichtmann U.Where formal verification can help in functional safety analysis.In:Proc.of the 2016 IEEE/ACM Int'l Conf.on Computer-aided Design (ICCAD).ACM, 2016.1-8.
    [5] Alrajeh D, Kramer J, Russo A, et al.Elaborating requirements using model checking and inductive learning.IEEE Trans.on Software Engineering, 2012, 39(3):361-383.
    [6] Ammann PE, Black PE, Majurski W.Using model checking to generate tests from specifications.In:Proc.of the 2nd Int'l Conf.on Formal Engineering Methods.IEEE, 1998.46-54.
    [7] Fuxman A, Pistore M, Mylopoulos J, et al.Model checking early requirements specifications in Tropos.In:Proc.of the 5th IEEE Int'l Symp.on Requirements Engineering.IEEE, 2001.174-181.
    [8] Heitmeyer C, Kirby J, Labaw B, et al.Using abstraction and model checking to detect safety violations in requirements specifications.IEEE Trans.on Software Engineering, 1998, 24(11):927-948.
    [9] Visser W, Havelund K, Brat G, et al.Model checking programs.Automated Software Engineering, 2003, 10(2):203-232.
    [10] Xie F, Levin V, Browne JC.Model checking for an executable subset of UML.In:Proc.of the 16th Annual Int'l Conf.on Automated Software Engineering (ASE 2001).IEEE, 2001.333-336.
    [11] Xie F, Levin V, Browne JC.Objectcheck:A model checking tool for executable object-oriented software system designs.In:Proc.of the Int'l Conf.on Fundamental Approaches to Software Engineering.Berlin, Heidelberg:Springer, 2002.331-335.
    [12] Beyer D, Keremoglu ME.CPAchecker:A tool for configurable software verification.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2011.184-190.
    [13] Merz S.Model checking:A tutorial overview.Summer School on Modeling and Verification of Parallel Processes, 2000.3-38.
    [14] Kim M, Kim Y, Kim H.Unit testing of flash memory device driver through a SAT-based model checker.In:Proc.of the 23rd IEEE/ACM Int'l Conf.on Automated Software Engineering.IEEE, 2008.198-207.
    [15] Kim M, Kim Y, Kim H.A comparative study of software model checkers as unit testing tools:An industrial case study.IEEE Trans.on Software Engineering, 2010, 37(2):146-160.
    [16] Witkowski T, Blanc N, Kroening D, et al.Model checking concurrent Linux device drivers.In:Proc.of the 22nd IEEE/ACM Int'l Conf.on Automated Software Engineering.2007.501-504.
    [17] Dwyer MB, Carr V, Hines L.Model checking graphical user interfaces using abstractions.ACM SIGSOFT Software Engineering Notes, 1997, 22(6):244-261.
    [18] Dwyer MB, Tkachuk O, Visser W.Analyzing interaction orderings with model checking.In:Proc.of the 19th Int'l Conf.on Automated Software Engineering.IEEE, 2004.154-163.
    [19] Artho C, Garoche PL.Accurate centralization for applying model checking on networked applications.In:Proc.of the 21st IEEE/ACM Int'l Conf.on Automated Software Engineering (ASE 2006).IEEE, 2006.177-188.
    [20] Artho C, Leungwattanakit W, Hagiya M, et al.Cache-based model checking of networked applications:From linear to branching time.In:Proc.of the 2009 IEEE/ACM Int'l Conf.on Automated Software Engineering.IEEE, 2009.447-458.
    [21] Haydar M, Boroday S, Petrenko A, et al.Properties and scopes in Web model checking.In:Proc.of the 20th IEEE/ACM Int'l Conf.on Automated Software Engineering.2005.400-404.
    [22] Eisler S, Scheidler C, Josko B, et al.Preliminary results of a case study:Model checking for advanced automotive applications.In:Proc.of the Int'l Symp.on Formal Methods.Berlin, Heidelberg:Springer, 2005.533-536.
    [23] Vörtler T, Rülke S, Hofstedt P.Bounded model checking of Contiki applications.In:Proc.of the 15th IEEE Int'l Symp.on Design and Diagnostics of Electronic Circuits & Systems (DDECS).IEEE, 2012.258-261.
    [24] Yang MF, Gu B, Duan ZH, et al.Intelligent program synthesis framework and key scientific problems for embedded software.Chinese Space Science and Technology, 2022, 42(4):1-7(in Chinese with English abstract).
    [25] Gligoric M, Majumdar R.Model checking database applications.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Berlin, Heidelberg:Springer, 2013.549-564.
    [26] Song F, Touili T.Pushdown model checking for malware detection.Int'l Journal on Software Tools for Technology Transfer, 2014, 16(2):147-173.
    [27] Karna AK, Chen Y, Yu H, et al.The role of model checking in software engineering.Frontiers of Computer Science, 2018, 12(4):642-668.
    [28] Griggio A, Roveri M.Comparing different variants of the IC3 algorithm for hardware model checking.IEEE Trans.on Computer-Aided Design of Integrated Circuits and Systems, 2015, 35(6):1026-1039.
    [29] Biere A, Cimatti A, Clarke EM, et al.Symbolic model checking using SAT procedures instead of BDDs.In:Proc.of the 36th Annual ACM/IEEE Design Automation Conf.1999.317-320.
    [30] McMillan KL.Interpolation and SAT-based model checking.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2003.1-13.
    [31] Bradley AR.SAT-based model checking without unrolling.In:Proc.of the Int'l Workshop on Verification, Model Checking, and Abstract Interpretation.Berlin, Heidelberg:Springer, 2011.70-87.
    [32] Eén N, Mishchenko A, Brayton R.Efficient implementation of property directed reachability.In:Proc.of the 2011 Formal Methods in Computer-aided Design (FMCAD).IEEE, 2011.125-134.
    [33] Li J, Zhu S, Zhang Y, et al.Safety model checking with complementary approximations.In:Proc.of the 2017 IEEE/ACM Int'l Conf.on Computer-aided Design (ICCAD).IEEE, 2017.95-100.
    [34] Li J, Dureja R, Pu G, et al.Simplecar:An efficient bug-finding tool based on approximate reachability.In:Proc.of the Int'l Conf.on Computer Aided Verification.Cham:Springer, 2018.37-44.
    [35] HWMCC 2015.2015.http://fmv.jku.at/hwmcc15/
    [36] HWMCC 2017.2017.http://fmv.jku.at/hwmcc17/
    [37] Amla N, Du X, Kuehlmann A, et al.An analysis of SAT-based model checking techniques in an industrial environment.In:Proc.of the Advanced Research Working Conf.on Correct Hardware Design and Verification Methods.Berlin, Heidelberg:Springer, 2005.254-268.
    [38] Vizel Y, Gurfinkel A.Interpolating property directed reachability.In:Proc.of the Int'l Conf.on Computer Aided Verification.Cham:Springer, 2014.260-276.
    [39] Ivrii A, Gurfinkel A.Pushing to the top.In:Proc.of the 2015 Formal Methods in Computer-aided Design (FMCAD).IEEE, 2015.65-72.
    [40] Seufert T, Scholl C.Combining PDR and reverse PDR for hardware model checking.In:Proc.of the 2018 Design, Automation & Test in Europe Conf.& Exhibition (DATE).IEEE, 2018.49-54.
    [41] Dureja R, Gurfinkel A, Ivrii A, et al.IC3 with Internal signals.In:Proc.of the 2021 Formal Methods in Computer Aided Design (FMCAD).IEEE, 2021.63-71.
    [42] Seufert T, Scholl C, Chandrasekharan A, et al.Making PROGRESS in property directed reachability.In:Proc.of the Int'l Conf.on Verification, Model Checking, and Abstract Interpretation.Cham:Springer, 2022.355-377.
    [43] Brayton R, Mishchenko A.ABC:An academic industrial-strength verification tool.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2010.24-40.
    [44] Cimatti A, Clarke E, Giunchiglia E, et al.Nusmv 2:An opensource tool for symbolic model checking.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2002.359-364.
    [45] Kupferman O, Vardi MY.Model checking of safety properties.Formal Methods in System Design, 2001, 19(3):291-314.
    [46] Nieuwenhuis R, Oliveras A, Tinelli C.Solving SAT and SAT modulo theories:From an abstract davis-putnam-logemann-loveland procedure to DPLL (T).Journal of the ACM (JACM), 2006, 53(6):937-977.
    [47] Marques-Silva J, Lynce I, Malik S.Conflict-driven Clause Learning SAT Solvers.In:Handbook of Satisfiability.IOS Press, 2021.133-182.
    [48] Eén N, Sörensson N.An extensible SAT-solver.In:Proc.of the Int'l Conf.on Theory and Applications of Satisfiability Testing.Berlin, Heidelberg:Springer, 2003.502-518.
    [49] Audemard G, Simon L.Glucose:A solver that predicts learnt clauses quality.SAT Competition, 2009, 7-8.
    [50] Clarke EM.The birth of model checking.In:Grumberg O, Veith H, eds.25 Years of Model Checking Festschrift.LNCS 5000, Berlin, Heidelberg:Springer, 2008.1-26.
    [51] Burch JR, Clarke EM, McMillan KL, et al.Symbolic model checking:1020 states and beyond.Information and Computation, 1992, 98(2):142-170.
    [52] Yu Y, Subramanyan P, Tsiskaridze N, et al.All-SAT using minimal blocking clauses.In:Proc.of the 27th Int'l Conf.on VLSI Design and the 13th Int'l Conf.on Embedded Systems.IEEE, 2014.86-91.
    [53] Biere A, Claessen K.Hardware model checking competition.http://fmv.jku.at/hwmcc15/
    [54] Biere A.Aiger format.http://fmv.jku.at/aiger/FORMAT
    附中文参考文献
    [24] 杨孟飞, 顾斌, 段振华, 等.嵌入式软件智能合成框架及关键科学问题.中国空间科学技术, 2022, 42(4):1-7.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

于忠祺,张小禹,李建文.基于不可满足核的近似逼近可达性分析.软件学报,2023,34(8):3467-3484

复制
分享
文章指标
  • 点击次数:1047
  • 下载次数: 4072
  • HTML阅读次数: 2509
  • 引用次数: 0
历史
  • 收稿日期:2022-09-04
  • 最后修改日期:2022-10-13
  • 在线发布日期: 2022-12-30
  • 出版日期: 2023-08-06
文章二维码
您是第20252445位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号