模型检测中的模型抽象方法及其系统

摘要

本发明涉及模型检测中的模型抽象方法及系统，方法包括：步骤1，输入原始模型和指导属性；步骤2，为指导属性的每个节点求解其在原始模型中的超语义，根据超语义为指导属性的每个非叶子节点求解对应的基本序列；步骤3，对原始模型的状态空间建立划分；步骤4，应用指导属性、每个节点的超语义和每个非叶子节点的基本序列分割划分；步骤5，为指导属性的每个节点建立对应的证明模型，应用证明模型进一步分割步骤4分割后的划分；步骤6，由进一步分割后的划分生成原始模型对应的抽象模型。本发明能够在只提供指导属性的前提下，根据该指导属性自动地完成细化工作，同时使细划后的划分能够保留与指导属性相关的信息。

主权项

1. 一种模型检测中的模型抽象方法，其特征在于，包括：步骤1，输入原始模型和指导属性；步骤2，为所述指导属性的每个节点求解其在所述原始模型中的超语义，根据所述超语义为所述指导属性的每个非叶子节点求解对应的基本序列；步骤3，对所述原始模型的状态空间建立划分；步骤4，应用所述指导属性、每个所述节点的超语义和每个非叶子节点的基本序列分割所述划分；步骤5，为所述指导属性的每个节点建立对应的证明模型，应用所述证明模型进一步分割所述步骤4分割后的划分；步骤6，由进一步分割后的所述划分生成所述原始模型对应的抽象模型。