基于广义符号轨迹赋值模型验证的反例的产生

摘要：

广义符号轨迹赋值(Symbolic Trajectory Evaluation)引入了符号变量和抽象技术,解决了验证中状态爆炸的问题,但是却为寻找反例制造了很多障碍.针对此,提出了一种高效的寻找反例的算法,它应用集合的概念,通过回溯在父子路径之间进行集合的交集,可以高效地解决抽象引起的问题.并对此算法进行改进,解决了符号变量带来的问题.

关键词：广义符号轨迹赋值、反例、形式化验证、符号模型验证、抽象

所属期刊栏目：37

分类号：TP301.2(计算技术、计算机技术)

资助基金：国家自然科学基金60973016

在线出版日期：2010-11-03（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：245-248