一种基于中断序列图的中断驱动系统验证方法

摘要

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