-
题名基于模拟关系的精化检测方法
被引量：2
- 1
-
-
作者
王婷
陈铁明
刘杨
-
机构
浙江工业大学计算机科学与技术学院
School of Computer Engineering
-
出处
《软件学报》
EI
CSCD
北大核心
2016年第3期580-592,共13页
-
基金
国家自然科学基金(61103044
U1509214)
+1 种基金
浙江省自然科学基金(LQ15E050006
LY16F020035)~~
-
文摘
精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质,traces,stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,极大地提高了算法的性能,且该方法能够直接用于traces精化检测.在此基础上,提出了基于模拟关系的stable failures和failuresdivergence精化检测方法.此外,还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.
-
关键词
精化检测
模拟
FAILURES
DIVERGENCE
时间自动机
-
Keywords
refinement checking
simulation
failure
divergence
timed automata
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
