-
题名基于符号执行和LTL公式重写的测试用例产生方法
被引量：3
- 1
-
-
作者
陈冬火
刘全
-
机构
苏州大学计算机科学与技术学院
计算机软件新技术国家重点实验室(南京大学)
符号计算与知识工程教育部重点实验室(吉林大学)
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2013年第12期2661-2675,共15页
-
基金
国家自然科学基金项目(61070223
61103045
+3 种基金
61070122
61272005
61303108)
江苏省自然科学基金项目(BK2012616)
-
文摘
基于模型检验等形式化方法的测试用例自动产生技术成为测试自动化领域一项重要的进展.对于输入和输出为无界抽象数据类型的无限状态系统,利用传统模型检验技术难以有效地产生测试用例集合,提出基于符号执行和公式重写的测试用例产生方法.通过建立程序的符号化执行模型,避免输入和输出变量数值化枚举而导致的无限状态系统的建模和状态爆炸问题;建立基于符号化执行模型的时序公式重写规则,并根据线性时序逻辑(linear temporal logic,LTL)公式的反例模式求取复杂属性及行为约束关系,利用约束求解的方法自动产生测试用例集合.这种方法集成了符号执行技术和时序公式状态重写——一种轻量级模型检验技术,成为基于复杂抽象数据类型系统与属性相关的测试用例自动产生的有效方法.
-
关键词
测试用例自动产生
符号执行
公式重写
模型检验
线性时序逻辑
输入
输出符号变迁系统
-
Keywords
auto-generation of test cases
symbolic execution
formula rewriting
model checking
linear temporal logic （ltl）
input/output symbolic transition system （IOSTS）
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名LTL性质的可监视性
- 2
-
-
作者
王伟芳
樊丽丽
李宝凤
赵光峰
-
机构
唐山师范学院数学与计算科学学院
-
出处
《唐山师范学院学报》
2021年第3期18-20,共3页
-
基金
唐山师范学院科研基金项目(2016C12)。
-
文摘
以LTL的语义和可监视的定义为依据,证明了LTL性质的可监视性,得到了φ1∪φ2可监视的几个充分条件,还证明了可监视性在∨,■,○下是封闭的,在∪下不是封闭的。
-
关键词
可监视
ltl公式
模型检验
拓扑
-
Keywords
monitorable
ltl formula
model checking
topology
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种基于形式化验证的智能合约垄断行为检测方法
- 3
-
-
作者
宋茂源
-
机构
南京审计大学计算机学院
-
出处
《软件导刊》
2025年第5期115-121,共7页
-
基金
国家自然科学基金面上项目(71972102)
江苏省高等学校自然科学研究重大项目(20KJA520002)
江苏省高校优秀科技创新团队项目(2021)。
-
文摘
智能合约是区块链技术的重要应用,在数字经济中发挥着重要作用。智能合约本质上是程序代码,相关部门的监管较少,难以保证完全合法合规,可能会扰乱市场秩序,造成经济损失,一旦出现垄断行为会影响市场公平性和效率,进而损害用户权益。为此,以监测垄断行为出发点,提出一种基于形式化验证的智能合约垄断行为检测方法。首先,采用线性时序逻辑(LTL)表示法,将垄断中涉及的平等性、公正性属性形式化为相应公式;其次,将待检测的智能合约进行建模,利用SPIN工具验证智能合约是否满足定义的两种属性,以分析其是否违反了公平性属性。实验表明,该方法能较好地检测智能合约中的垄断行为,为智能合约的设计和审计提供了新思路。
-
关键词
智能合约
公平性
SPIN工具
ltl公式
垄断
-
Keywords
smart contract
fairness
SPIN tool
ltl formula
monopoly
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于Spin的安全协议形式化验证技术
被引量：4
- 4
-
-
作者
冉俊轶
吴尽昭
-
机构
中国科学院成都计算机应用研究所
中国科学院大学
广西混杂计算与集成电路设计分析重点实验室(广西民族大学)
北京交通大学计算机与信息技术学院
-
出处
《计算机应用》
CSCD
北大核心
2014年第A02期85-90,共6页
-
基金
国家自然科学基金资助项目(11371003)
广西自然科学基金资助项目(2011GXNSFA018154
+2 种基金
2012GXNSFGA060003)
广西区主席科技资金资助项目(10169-1)
广西教育厅科研资助项目(201012MS274)
-
文摘
针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑(LTL)公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协议改进方案,并针对改进后的协议,给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法:模型检测过程中的存储状态数减少,使模型复杂度降低约40%;迁移状态数减少,使验证效率提升约44%。
-
关键词
安全协议
形式化验证
Spin模型检测
Promela语义模型
ltl公式
密钥分配中心协议
-
Keywords
security protocol
formal verification
Spin model checking
Promela semantic model
Linear Timing Logic（ltl） formula
key contribution center protocol
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-
