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

龙图腾网获悉卡斯柯信号(成都)有限公司申请的专利一种用于联锁软件形式化验证的系统模型构建方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN115562669B 。

龙图腾网通过国家知识产权局官网在2025-07-11发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202211318834.8，技术领域涉及：G06F8/38；该发明授权一种用于联锁软件形式化验证的系统模型构建方法是由张铭瑶;王燕芩;杨平;张程;徐军强;朱迎春;杨帆;季雯婷设计研发完成，并于2022-10-26向国家知识产权局提交的专利申请。

本一种用于联锁软件形式化验证的系统模型构建方法在说明书摘要公布了：本发明公开了一种用于联锁软件形式化验证的系统模型构建方法，涉及计算机联锁系统技术领域。本发明利用采用不同的编程方法和编程语言开发的两个具有相同功能的翻译器读取联锁输入数据；并通过文件比较工具对两个具有相同功能的翻译器输出的特点格式的数据文件进行一致性校验；采用编程方法开发一个系统模型构建工具，利用该系统模型构建工具读入S1步骤中经翻译器数据转换后且通过一致性校验的特定格式文件，依据特定格式文件构建系统模型。本发明从信号人员视角出发，重点描述联锁数据层面的系统模型构建，及其与对象模型的映射关系。本发明描述的系统模型构建方法为信号人员如何依据现有联锁数据构建系统模型提供了一种思路。

本发明授权一种用于联锁软件形式化验证的系统模型构建方法在权利要求书中公布了：1.一种用于联锁软件形式化验证的系统模型构建方法，其特征在于，该构建方法包括以下步骤： S1、采用不同的编程方法和编程语言开发的两个具有相同功能的翻译器读取联锁输入数据；所述联锁输入数据包括站场拓扑结构文件、TAB表格文件和布尔逻辑文件；两个具有相同功能的翻译器将联锁输入数据转换为特定格式的数据文件，并通过文件比较工具对两个具有相同功能的翻译器输出的特定格式的数据文件进行一致性校验； S2、采用编程方法开发一个系统模型构建工具，利用该系统模型构建工具读入S1步骤中经翻译器数据转换后且通过一致性校验的特定格式文件，依据特定格式文件构建系统模型； S3、依据站场拓扑结构文件转换后的特定格式文件构建站场拓扑模型： S301、创建节点和边组成的有向图结构，依据站场拓扑结构文件转换后的特定格式文件中设备连接关系，将每个设备用同一个同等类型的节点占位，每个节点定义其id和节点类型，形成节点模块； S302、通过边将节点串接成图结构，将节点与节点的连接关系两两一组定义到边模块中； S303、将站场设备对象存储于对应的节点中，形成对象模块，对象模块生成每个设备对象所在节点的节点id； S304、依据站场拓扑结构文件转换后的特定格式文件中的进路表信息，生成进路模块； S305、依据站场图区域内设备信息，生成区域模块； 节点模块、边模块、对象模块、进路模块和区域模块构成完整的站场拓扑模型； S4、依据TAB表格文件转换后的特定格式文件构建对象关系模型： S401、依据TAB表格文件转换后的特定格式文件中各子表定义一级表格，同时，将站场拓扑结构文件转换后的特定格式文件中的信号设备子表和进路表按照一级表格进行定义；按照一级表格定义的子表包含该特定格式文件中对应子表的全部列； S402、依据用于形式化验证用的对象模型中的关系定义二级表格；建立二级表格与对象关系的映射关系，将对象模型的关系追踪到二级表格中；生成用于形式化验证的对象关系模型； S5、依据布尔逻辑文件转换后的特定格式文件构建布尔变量模型，具体的，依据用于形式化验证用的对象模型中的对象变量，人工配置变量关系映射文件，建立对象变量与布尔逻辑文件转换后的特定格式文件中的实际布尔变量的一对一映射；生成用于形式化验证的布尔变量模型。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人卡斯柯信号(成都)有限公司，其通讯地址为：610036 四川省成都市金牛区金牛高新技术产业园区金凤凰大道666号13栋1单元1楼1号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。