公开(公告)号：CN104503837A

公开(公告)日：2015-04-08

申请号：CN201510019677.4

申请日：2015-01-15

Applicant: 南京大学

Inventor： 赵建华 ,  蔡增科 ,  戎挺

IPC: G06F9/48

Abstract: 基于偏序规约的中断驱动系统有界模型检验方法，该方法采用偏序规约来约减中断驱动系统有界模型检验状态遍历过程中的路径和状态。本发明根据中断驱动系统所具有的性质，首先定义中断处理程序之间的依赖关系；然后通过静态分析，得到中断处理程序之间的相互依赖关系，并用矩阵表示；最后在状态空间遍历过程中，当全局状态上有多个中断同时满足触发条件时，将这些中断根据相互依赖关系生成偏序路径，并按照此路径执行到达新的全局状态。本发明的目的是约去冗余的遍历路径，约减状态空间，缩短验证时间。本发明具有广泛的适用性，能大幅减少中断驱动系统的模型检验时间，适用于包含较多中断数量的中断驱动系统。

公开(公告)号：CN104503837B

公开(公告)日：2017-10-10

申请号：CN201510019677.4

申请日：2015-01-15

Applicant: 南京大学

Inventor： 赵建华 ,  蔡增科 ,  戎挺

IPC: G06F9/48

Abstract: 基于偏序规约的中断驱动系统有界模型检验方法，该方法采用偏序规约来约减中断驱动系统有界模型检验状态遍历过程中的路径和状态。本发明根据中断驱动系统所具有的性质，首先定义中断处理程序之间的依赖关系；然后通过静态分析，得到中断处理程序之间的相互依赖关系，并用矩阵表示；最后在状态空间遍历过程中，当全局状态上有多个中断同时满足触发条件时，将这些中断根据相互依赖关系生成偏序路径，并按照此路径执行到达新的全局状态。本发明的目的是约去冗余的遍历路径，约减状态空间，缩短验证时间。本发明具有广泛的适用性，能大幅减少中断驱动系统的模型检验时间，适用于包含较多中断数量的中断驱动系统。