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

龙图腾网获悉上交所技术有限责任公司申请的专利一种面向核心交易系统架构代码实现的抽象建模及验证方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN119782125B 。

龙图腾网通过国家知识产权局官网在2025-07-08发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202510285990.6，技术领域涉及：G06F11/3604；该发明授权一种面向核心交易系统架构代码实现的抽象建模及验证方法是由颜彧;杜德慧;韩大伟;李行;李尔牧云;李光强;刘凯;林征设计研发完成，并于2025-03-12向国家知识产权局提交的专利申请。

本一种面向核心交易系统架构代码实现的抽象建模及验证方法在说明书摘要公布了：本发明是一种面向核心交易系统架构代码实现的抽象建模及验证方法，包括：A对交易系统的架构进行建模与验证：通过从架构框架的代码实现与开发设计文档中抽取相关信息，使用抽象建模技术构建已有系统的行为模型，利用UML顺序图建模系统的进程通信过程，将UML顺序图转换成CSP的形式化模型，并使用PAT验证器进行安全性质的验证分析；B对交易系统中集群选主模块进行建模及验证：构建集群选主过程中各个节点的状态机模型，构建系统动态模型，并使用PAT验证器对选主过程的正确性进行验证分析。本发明优点在于：解决交易系统架构中各进程间通信过程及集群选主过程中各个节点的状态变迁建模问题，提升建模及安全性验证分析能力。

本发明授权一种面向核心交易系统架构代码实现的抽象建模及验证方法在权利要求书中公布了：1.一种面向核心交易系统架构代码实现的抽象建模及验证方法，其特征在于，所述方法包括： A.对交易系统的架构进行建模与验证： 通过从架构框架的代码实现与开发设计文档中抽取相关信息，使用抽象建模技术构建已有系统的行为模型，利用UML顺序图建模系统的进程通信过程，将UML顺序图转换成CSP的形式化模型，用于描述系统的通信机制与同步行为，并使用PAT验证器进行安全性质的验证分析； B.对交易系统中集群选主模块进行建模及验证： 构建集群选主过程中各个节点的状态机模型，用以描述集群选主的状态变迁过程，构建系统动态模型，并使用PAT验证器对选主过程的正确性进行验证分析； 所述对交易系统中集群选主模块进行建模及验证的方法具体如下： S1.基于UML状态机图建模核心交易系统的集群选主模块,包括： S11.对集群选主模块的代码实现逻辑进行分析，抽象出集群节点在选主过程中可能出现的不同工作状态； S12.深入研究节点的状态变迁逻辑，并通过UML状态机模型明确定义各节点在不同状态之间的转移条件及其对应的触发事件或操作； S13.结合集群选主模块的设计文档及实际代码实现，对状态机图进行比对与验证，确保状态机图准确反映了节点行为的实际情况，从而避免潜在的逻辑错误或不一致性； S2.集群选主模块的CSP模型，包括： S21.将状态机图中的状态变迁与操作映射为CSP模型中的事件序列，不同的迁移条件通过并发算子组合起来； S22.考虑到集群中的节点可能出现故障，CSP模型中加入故障状态； S23.通过断言的方式定义性质规约，针对状态机图的性质规约有活性、安全性以及稳定定性； S3.利用PAT模型验证器进行验证，在构建了CSP形式化模型后，使用PAT模型验证器对CSP模型进行验证，确保系统满足预定义的性质要求，所述性质包括活性、安全性以及稳定性，通过在PAT验证器中使用#assert断言语句形式化定义上述规约，对模型的关键行为进行全面验证； 所述对交易系统中集群选主模块进行建模及验证的方法还包括步骤S4.CSP形式化模型优化与反馈迭代，根据PAT验证的反馈结果，进行优化与反馈，确保系统设计能够在每次迭代中得到改进。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人上交所技术有限责任公司，其通讯地址为：200131 上海市浦东新区中国(上海)自由贸易试验区台中北路8号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。