基于SMT的TECTL性质的限界模型检测方法

J4 ›› 2013, Vol. 35 ›› Issue (10): 166-171.

基于SMT的TECTL性质的限界模型检测方法

徐亮，刘宏

(1. 湖南师范大学数学与计算机科学学院，湖南长沙 410081;
2.高性能计算与随机信息处理省部共建教育部重点实验室，湖南长沙 410081)

收稿日期:2013-03-06 修回日期:2013-05-24 出版日期:2013-10-25 发布日期:2013-10-25
基金资助:
国家自然科学基金资助项目（60903168）；湖南省教育厅科学研究项目（13C527）；湖南省科技计划资助项目(2012FJ6012)；长沙市科技计划资助项目(K110902011);湖南省重点学科建设资助项目（湘教发［2011］76号）

Bounded model checking of
TECTL properties based on SMT

XU Liang，LIU Hong

(1.College of Mathematics and Computer Science,Hunan Normal University,Changsha 410081;
2.Key Laboratory of High Performance Computing and Stochastic Information Processing,
Ministry of Education of China,Changsha 410081,China)

Received:2013-03-06 Revised:2013-05-24 Online:2013-10-25 Published:2013-10-25

摘要/Abstract

摘要：

近些年来，基于SMT的限界模型检测方法作为基于SAT的限界模型检测方法的一种改进，在对实时系统的检测上已经得到了一定发展。一直以来，限界模型检测多被用于检验存在性性质，而很少用于验证全局性性质，原因之一就是该方法受界限的限制，很难实现对全局性性质的有效编码。为此，通过对传统限界模型检测中的编码方式进行相应改变，在一定程度上解决了这一问题。同时，结合SMT，实现了对实时系统中某些全局性性质的验证。实验表明该方法比已有的方法效率更高。

关键词: 限界模型检测, 可满足性模理论, 全局性性质, 实时系统, 验证

Abstract:

Satisfiability Modulo Theories (SMT)based bounded model checking (BMC) has been considered as an improved technique to SATbased bounded model checking in recent years. Bounded model checking has often been used to check existential properties, but rarely used to verify global properties, and one of the reasons is that this method is hard to encode the global properties as its’ restricted by the bound. Therefore, In order to verify the global properties, the encodings in traditional bounded model checking should be changed. Combining with SMT, some global properties can be verified in real time systems. Experiments demonstrate the method is more efficient than existing methods.

Key words: bounded model checking;SMT;global properties;real time systems;verification

徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.

XU Liang，LIU Hong. Bounded model checking of
TECTL properties based on SMT [J]. J4, 2013, 35(10): 166-171.

[1]	唐傲, 王晓峰, 何飞. 可满足性模理论综述[J]. 计算机工程与科学, 2024, 46(03): 400-415.
[2]	赵祉乔, 周理, 荀长庆, 潘国腾, 铁俊波, 王伟征 . 软硬件混合的高效CHI协议分析[J]. 计算机工程与科学, 2024, 46(02): 224-231.
[3]	邓茜, 范广生, 陈立前, 李暾, 王戟. 基于C语言程序分析验证技术的Verilog代码验证方法[J]. 计算机工程与科学, 2023, 45(12): 2146-2154.
[4]	刘永梅, 王国辉, 关永, 张景芝, 施智平, 董璐. 格林定理的形式化及其初步应用[J]. 计算机工程与科学, 2023, 45(07): 1178-1187.
[5]	白先平, 姚袭欣, 陈香兰, 刘翀, 李曦. 基于时间自动机的AADL端到端流规约验证方法[J]. 计算机工程与科学, 2023, 45(05): 810-819.
[6]	罗莉, 石伟, 何鸿君, 潘国腾, 王蕾, 龚锐. 一种面向IO Die的敏捷验证方法[J]. 计算机工程与科学, 2023, 45(04): 571-576.
[7]	姚袭欣, 章博, 陈香兰, 乔磊, 李曦. 一种基于Event-B语言的时间触发系统建模方法[J]. 计算机工程与科学, 2023, 45(04): 613-621.
[8]	汪铮, 黄容, 吴茂文, 孙寅涵, 孙志刚. OpenEmulator:一种面向TSN芯片验证的联合仿真平台[J]. 计算机工程与科学, 2023, 45(03): 411-419.
[9]	寇广岳, 魏国珩, 平源, 刘鹏. RFID安全认证协议综述[J]. 计算机工程与科学, 2023, 45(01): 77-84.
[10]	王雨露, 李飞, 杨震, 黄山, 张罡, 詹曙, . 基于深度前馈神经网络的多因子人体表面积计算模型[J]. 计算机工程与科学, 2023, 45(01): 119-126.
[11]	陈强, 谭林, 王云丽, 肖靖. 工业区块链中基于CUDA的数据并行处理方法[J]. 计算机工程与科学, 2022, 44(12): 2102-2110.
[12]	牛淑芬, 张美玲, 周思玮, 闫森. 面向移动终端的密文可验证属性基可搜索加密方案[J]. 计算机工程与科学, 2022, 44(11): 1941-1950.
[13]	李辉, 巨鹏锦, 计永兴. 多路系统Cache一致性验证中的错误追踪定位技术[J]. 计算机工程与科学, 2022, 44(07): 1171-1180.
[14]	陈小帆, 杨智杰, 彭凌辉, 王世英, 周干, 李石明, 康子扬, 王耀, 石伟, 王蕾. 一种类脑处理器片上网络的验证框架[J]. 计算机工程与科学, 2022, 44(05): 769-778.
[15]	邹鸿基, 李暾, 罗丹, 方雨德. 面向敏捷硬件设计的符号模拟器设计与实现[J]. 计算机工程与科学, 2021, 43(12): 2098-2104.