公开(公告)号：CN110175019A

公开(公告)日：2019-08-27

申请号：CN201910480184.9

申请日：2019-06-04

Applicant: 南京大学

Inventor： 潘敏学 ,  陈守煜 ,  张天 ,  王林章 ,  李宣东

IPC: G06F8/10

Abstract: 本发明公开了一种基于中断序列图的中断驱动系统验证方法，包括如下步骤，步骤1：基于中断序列图来建立中断驱动系统模型；步骤2：根据步骤1得到的中断序列图，将其中的交互片段划分为基本交互和复合交互片段；步骤3：将基本交互片段和复合交互片段依次转换成自动机；步骤4：将步骤3中得到的多个自动机组合成一个混成自动机；步骤5：提取中断序列图的约束，将约束添加到转换得到的自动机模型上；步骤6：提取中断序列图中的验证属性信息，将验证属性作为约束添加到转换得到的自动机模型上；步骤7：将自动机描述成自动机验证工具可接受的输入格式；步骤8：采用自动机验证工具进行验证。

公开(公告)号：CN110175019B

公开(公告)日：2021-11-16

申请号：CN201910480184.9

申请日：2019-06-04

Applicant: 南京大学

Inventor： 潘敏学 ,  陈守煜 ,  张天 ,  王林章 ,  李宣东

IPC: G06F8/10

Abstract: 本发明公开了一种基于中断序列图的中断驱动系统验证方法，包括如下步骤，步骤1：基于中断序列图来建立中断驱动系统模型；步骤2：根据步骤1得到的中断序列图，将其中的交互片段划分为基本交互和复合交互片段；步骤3：将基本交互片段和复合交互片段依次转换成自动机；步骤4：将步骤3中得到的多个自动机组合成一个混成自动机；步骤5：提取中断序列图的约束，将约束添加到转换得到的自动机模型上；步骤6：提取中断序列图中的验证属性信息，将验证属性作为约束添加到转换得到的自动机模型上；步骤7：将自动机描述成自动机验证工具可接受的输入格式；步骤8：采用自动机验证工具进行验证。