买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网恭喜西安邮电大学申请的专利一种可视化模型检测方法、系统、介质、设备及处理终端获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN115145573B 。

龙图腾网通过国家知识产权局官网在2025-05-16发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202210216199.6，技术领域涉及：G06F8/41；该发明授权一种可视化模型检测方法、系统、介质、设备及处理终端是由舒新峰;李彦霖;王曙燕;孙家泽;杨泽伟;贾怡阳设计研发完成，并于2022-03-06向国家知识产权局提交的专利申请。

本一种可视化模型检测方法、系统、介质、设备及处理终端在说明书摘要公布了：本发明属于系统形式化建模与验证技术领域，公开了一种可视化模型检测方法、系统、介质、设备及处理终端，使用可视化建模语言xUML4MC建立系统设计模型，使用OPSL以注释方式在设计模型中标注类、方法、语句段及语句具备的性质特征；对设计模型进行词法语法分析，构造附加OPSL性质的抽象语法树；将每个OPSL语句转换为PPTL性质公式并取非后构造出性质非自动机CFA；执行抽象语法树动态生成系统状态，按OPSL语句约束位置和对应CFA进行与运算，构造出结果自动机，如果存在可接受路径则为性质不成立的反例路径，否则性质成立。本发明弥补了对UML设计模型的直接模型检测，促进模型检测技术在工业界的推广使用。

本发明授权一种可视化模型检测方法、系统、介质、设备及处理终端在权利要求书中公布了：1.一种可视化模型检测方法，其特征在于，所述可视化模型检测方法使用xUML4MC建立系统模型，使用OPSL以注释方式在系统模型中标注类、方法、语句段及语句具备的性质特征；对系统模型进行词法和语法分析，构造附加OPSL性质的抽象语法树，并进行完整性、一致性校验；将抽象语法树中每个OPSL语句转换为PPTL性质公式并取非后构造出对应性质非自动机CFA；执行抽象语法树动态生成系统状态，并按OPSL语句约束位置和对应CFA进行与运算，构造出结果自动机，如果存在可接受路径则为性质不成立的反例路径，否则性质成立；所述在xUML4MC系统模型中使用OPSL以注释方式标注系统性质的规则包括：规则1：将一个类所有对象从创建完成到销毁前为止所应具备的性质，使用OPSL语句进行描述后，并在类图中通过xUML4MC的注释符号标注在对应的类节点上，简称“类性质”；规则2：将一个函数在执行期间具备的性质，使用OPSL语句进行描述后，并在该函数对应活动图中通过xUML4MC的注释符号标注在起始节点上，简称“函数性质”；规则3：将一个函数中的语句片段在执行期间具备的性质，使用OPSL语句进行描述，并在该函数对应活动图中通过xUML4MC的注释符号标注在对应语句片段的开始节点和结束节点上，简称“语句片段性质”；规则4：将函数中一条语句在执行期前具备的性质，使用OPSL语句进行描述，并在该函数活动图中通过xUML4MC的注释符号标注在对应语句节点上，简称“断言性质”；所述附加OPSL性质的抽象语法树构造方法包括：1从xUML4MC系统模型的类图、活动图中提取模型元素及关系；2对模型元素进行词法分析、语法分析，创建对应抽象语法树节点；3依据可视化模型元素的继承、关联、组合、聚合、注释关系，将语法树节点构成语法树；4从xUML4MC系统模型的类图和互动图的注释中提取OPSL语句，并进行词法语法、分析，构造OPSL语句的语法树，并按照OPSL的约束位置附加到抽象语法树的对应节点上；所述抽象语法树的完整性和一致性校验规则包括：规则5：方法活动图与类图的一致性，包括方法名称、参数类型及个数；方法内部变量名的有效性，或者为类含继承属性，或为方法形式参数，或为定义的局部变量；规则6：OPSL语句的校验，包括语法符合OPSL语法定义和引用变量名是否正确，其中类性质只能引用类自定义的属性或继承的属性，其他三种只能引用类的属性，方法的形参及定义的局部变量；所述将PPTL性质公式取非后构造出对应的性质非自动机CFA包括：1.1对于PPTL性质公式进行预处理，将其中所有包含的子公式□P替换为子公式◇P替换为true；P，子公式P1→P2替换为子公式替换为P；1.2计算出PPTL性质公式所包含的原子命题集合Φ，CFA的字母表1.3构造PPTL性质公式P的CFA，规则包括：规则1.3.1：若性质公式为原子命题p，p的CFA为Ap＝∑,Q,δ,I,F,C，其中状态集合Q＝{q0,q1}，迁移集合δ＝{q0,p,q1,q0,true,q1}，初始状态集合I＝{q0}，有穷可接受集合F＝{q1}，无穷可接受条件集合C＝{{q1}}；规则1.3.2：若性质公式为P1∨P2，先分别构造出P1和P2的CFA，令其分别为AP1＝∑,Q1,δ1,I1,F1,C1和AP2＝∑,Q2,δ2,I2,F2,C2，最终的CFA为AP1∨P2＝∑,Q1∪Q2,δ1∪δ2,I1∪I2,F1∪F2,C1∪C2；规则1.3.3：若性质公式为P1∧P2，先分别构造出P1和P2的CFA，令其分别为AP1＝∑,Q1,δ1，I1,F1,C1和AP2＝∑,Q2,δ2,I2,F2,C2，最终的CFA为AP1∧P2＝∑,Q,δ,I,F,C，其中Q＝{[q1,q2]|q1∈Q1,q2∈Q2}，I＝{[q1,q2]|q1∈I1,q2∈I2}，F＝{[q1,q2]|q1∈F1,q2∈F2}，C＝{{[q1,q2]|q1∈Δ1,q2∈Δ2}|Δ1∈C1,Δ2∈C2}；规则1.3.4：若性质公式为P1；P2，先分别构造出P1和P2的CFA，令其分别为和AP2＝Σ,Q2,δ2,I2,F2,C2，最终的CFA为AP1；P2＝∑,Q1∪Q2,δ1∪δ2∪δaI1，F2,C2，其中 规则1.3.5：若性质公式为先构造出P1的CFAAP1＝∑,Q1,δ1，I1，F1,C1，最终的CFA为其中 且 规则1.3.6：若性质公式为先构造出P1的CFAAP1＝∑,Q1,δ1，I1，F1,C1，并使用子集构造法将AP1转换为确定CFA最终的CFA为为所述执行抽象语法树动态生成系统状态，并按OPSL语句约束位置和对应的CFA进行与运算，构造出结果自动机，如果结果自动机中不存在可接受路径则性质成立，否则可接受路径为性质不成立的反例路径，具体方法包括：2.1使用抽象语法树指定模型检测验证的入口函数fun初始化结果自动机rstCFA＝Σ,Q,δ,I,F,C，自动机状态为二元组stmt,stateSet，stmt为抽象语法树中语句，stateSet为对应性质自动机状态集合，Q＝{fun,{}}，I＝{fun,{}}，将rstCFA的初始状态fun,{}压入回溯栈，指定fun作为当前验证函数；2.2根据当前验证函数中标注的OPSL语句计算带约束位置的性质非自动机二元组cfa,start:end集合CFASet，其中cfa为性质非自动机，start和end为cfa约束的起始位置和截止位置；2.3若当前函数标注OPSL函数性质语句prop，构造二元组cfa,start:end加入到CFASet中，其中cfa为prop对应性质非自动机，start等于该函数的第一条语句位置，end等于该函数的最后一条语句位置；2.4取出回溯栈的栈顶元素stmt,stateSet，对于CFASet中的所有性质非自动机二元组cfa,start:end，若start等于stmt，令stateSet＝stateSet∪I，其中I为cfa的初始状态集合；执行栈顶元素的stmt语句，令结果为rst；2.5若则转步骤2.8，否则依次取出stateSet中的每个cfa状态q，枚举从q状态出发的未搜索弧q,α,q1，转步骤2.6；2.6使用Z3求解器计算rst与α合取公式的可满足性，如果结果为false，转步骤2.9；否则，按照抽象语法树执行规则取出stmt语句的下一条待执行语句stmt1，动态扩展结果自动机rstCFA，规则包括：规则2.6.1：若rstCFA中存在状态stmt1,stateSet1和弧stmt0,stateSet0,rst,stmt1,stateSet1且q1∈stateSet1，计算rstCFA中从状态stmt1,stateSet1到状态stmt,stateSet的路径上所有stateSet的并集sset，如果CFASet中存在一个cfa的一个无穷接收条件c满足将回溯栈中状态序列为添加到反例路径集合CountExamPathSet中，转步骤2.9；规则2.6.2：若规则2.6.1条件不成立，在rstCFA的状态集合Q中添加新状态stmt1,{q1}，在迁移集合δ中增加新弧stmt,stateSet,rst,stmt1,{q1}；如果CFASet中存在性质非自动机二元组cfa,start:end满足stmt1等于end且q1为cfa的一个有穷可接收状态，即q1∈F，将回溯栈中状态序列为添加到反例路径集合CountExamPathSet中；将状态stmt1,{q1}压入回溯栈，转步骤2.4；2.7如果stateSet中存在未搜索弧q,α,q1，则转步骤2.5，否则转步骤2.9；2.8按照抽象语法树执行规则取出stmt语句的下一条待执行语句stmt1，动态扩展结果自动机rstCFA，规则包括：规则2.8.1：若rstCFA中存在状态stmt1,stateSet1和弧stmt0,stateSet0,rst,stmt1,stateSet1，转步骤2.9；规则2.8.2：若规则2.8.1条件不成立，在rstCFA的状态集合Q中添加状态stmt1,{}，在迁移集合δ中增加弧stmt,{},rst,stmt1,{}；将状态stmt1,{}压入回溯栈，转步骤2.4；2.9将回溯栈顶元素stmt,stateSet出栈，并从rstCFA中将状态stmt,stateSet及其关联的弧删除掉；如果回溯栈不为空，转步骤2.4，否则转步骤2.10；2.10如果反例路径集合输出待验证性质成立，否则逐个输出CountExamPathSet中保存的反例路径；所述步骤2.2中根据该函数上标注的OPSL语句计算带约束位置的性质非自动机二元组cfa,start:end集合CFASet，按照深度优先策略遍历该函数的每一条语句，计算带约束位置的性质非自动机二元组并加入到CFASet，具体规则包括：规则2.2.1：若当前类标注OPSL类性质prop，构造二元组cfa,start:end加入到CFASet中，该二元组的start等于标注prop的语句的下一条语句位置，end等于该对象销毁前的一条语句位置；规则2.2.2：若当前代码片段标注OPSL代码段性质的起始性质语句prop_start和结束性质语句prop_end，构造二元组cfa,start:end加入到CFASet中，该二元组的start等于标注prop_start的语句的下一条语句位置，end等于标注prop_end的语句位置；规则2.2.3：若当前代码片段标注OPSL断言性质prop，构造二元组cfa,start:end加入到CFASet中，该二元组的start等于标注prop的语句的位置，end等于标注prop的语句位置；所述步骤2.4中执行栈顶元素的stmt语句，令结果为rst；执行规则包括：规则2.4.1：对于普通语句节点，选取当前节点的后继节点为下一个待执行语句节点；规则2.4.2：对于if语句节点，计算if语句中条件表达式的值，根据结果真、假选取对应YES、NO分支的第一个节点为下一个待执行语句节点；规则2.4.3：对于while语句节点，计算while语句中条件表达式的值，如果结果为真则选取YES分支的第一个节点为下一个待执行节点，否则选取while循环的后继节点为下一个待执行语句节点；规则2.4.4：对于函数调用语句节点，计算各实参表达式值并赋给对应函数形式参数后，将被调用函数第一条语句作为下一个待执行语句节点。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人西安邮电大学，其通讯地址为：710061 陕西省西安市雁塔区长安南路563号西安邮电大学；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。