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

龙图腾网获悉北京交通大学申请的专利从Simulink-StateFlow模型到NuSMV模型的转换方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN115391173B 。

龙图腾网通过国家知识产权局官网在2025-07-22发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202210789598.1，技术领域涉及：G06F11/3604；该发明授权从Simulink-StateFlow模型到NuSMV模型的转换方法是由杜晔;吴润方;黎妹红;吴雪松;张乐设计研发完成，并于2022-07-06向国家知识产权局提交的专利申请。

本从Simulink-StateFlow模型到NuSMV模型的转换方法在说明书摘要公布了：本发明涉及一种从Simulink‑StateFlow模型到NuSMV模型的转换方法，包括如下步骤：对待评估系统进行需求分析，构建Simulink‑StateFlow模型；提取模型中的程序语句、自定义函数语句、逻辑顺序关系，分别构建程序语句数据表、自定义函数数据表、逻辑顺序数据表；整合模型程序及顺序，生成模型信息表；对Matlab编程语言进行分析，构建Matlab语法规则；根据语法规则对模型信息表中的程序语句进行处理，将其解析为抽象语法树；对抽象语法树进行处理，确定转换为NuSMV语句的算法；根据转换算法处理模型信息表，生成NuSMV模型。本发明大大提高了NuSMV工具对Simulink‑StateFlow模型进行模型检测的效率和准确度，实现对控制系统Simulink需求模型的安全性验证。

本发明授权从Simulink-StateFlow模型到NuSMV模型的转换方法在权利要求书中公布了：1.一种从Simulink-StateFlow模型到NuSMV模型的转换方法，其特征在于，包括如下步骤： 步骤1、对待评估的系统进行需求形式化分析，并构建Simulink-StateFlow模型；生成项目工程文件，项目工程文件包括：JSON格式文件、C语言格式文件和SVG格式文件； 步骤2、分析JSON格式文件的格式特征，从JSON格式文件中提取程序语句，构建程序语句数据表； 步骤3、分析C语言格式文件的格式特征，从C语言格式文件中提取自定义函数语句，构架自定义函数数据表； 步骤4、分析SVG格式文件的格式特征，读取步骤2中提取到的程序语句的逻辑顺序关系，构建逻辑顺序数据表； 步骤5、根据步骤2、步骤4中构建的程序语句数据表和逻辑顺序数据表，使用算法整合模型程序及顺序，生成Simulink模型信息表； 步骤6，对程序语句所使用的Matlab编程语言进行分析，构建Matlab语言的语法规则； 步骤7，根据步骤6给出的Matlab语言的语法规则对Simulink模型信息表中的程序语句进行处理，将程序语句解析为抽象语法树AST； 步骤8，对抽象语法树AST进行处理，确定转换为NuSMV语句的转换算法；根据转换算法，处理Simulink模型信息表，生成NuSMV模型,具体如下： 步骤801、自动化转换定义与初始化语句；转换过程中，待转换程序语句支持的基本类型包括整数型、实数型、字符数据、逻辑值型、阵列数据、Matlab-Simulink的内置函数及使用Matlab编辑器编写的自定义函数，整数型包括多位有符号字和无符号字整数，实数型包括单精度浮点数和双精度数浮点数；NuSMV支持类型包括布尔型、整数型、枚举型、有符号字、无符号字、数组型和set类型； 其中，程序语句中的逻辑值型与NuSMV中的布尔型对应；程序语句中的整数型与NuSMV中的整数型对应；程序语句中的单精度浮点数与NuSMV中的有符号字对应；程序语句中的双精度浮点数与NuSMV中的无符号字对应； 程序语句中的状态变量直接映射到NuSMV的状态变量，且类型相同，名称保持不变；环境变量的转换取决于状态变量，在模型转换过程中根据实际情况，将环境变量先通过状态变量表述，然后再对状态变量进行转换； 步骤802、将自定义函数转换为NuSMV中的模块；自定义函数同样使用Matlab编程语言编写；对于函数语句中算数运算符的转换，需要同时对结果进行验证，使其符合NuSMV常量的取值范围；在NuSMV验证的过程中，只有验证模型中能够被NuSMV识别的Matlab函数会被调用参与运算和执行，其他在书写程序语句及自定义函数时使用的Matlab内置函数不可被识别，需要在语法分析的过程中被筛选定位，将其单独转换为可识别的语句或程序步骤；而后将转换后的自定义函数体返回； 步骤803、判断语句类型，自动转换赋值语句、循环语句和判断语句；对于循环及判断语句，NuSMV中使用case表达式描述条件的转移过程，将待转换状态模型中的每一条转移映射为NuSMV中的条件表达式；针对状态模型中的每一个待定状态，找出状态模型中所有改变NuSMV环境变量的赋值行为，并将其转换为对应的case子句； 步骤804、生成转换后的NuSMV模型。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人北京交通大学，其通讯地址为：100044 北京市海淀区上园村3号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。