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

龙图腾网恭喜中铁第六勘察设计院集团有限公司;中国国家铁路集团有限公司申请的专利基于Event-B的Java代码自动生成中内存安全验证方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN119782124B 。

龙图腾网通过国家知识产权局官网在2025-05-09发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202510272147.4，技术领域涉及：G06F11/3604；该发明授权基于Event-B的Java代码自动生成中内存安全验证方法是由王烨;范建国;李栋;付功云;王婷;杨喆设计研发完成，并于2025-03-10向国家知识产权局提交的专利申请。

本基于Event-B的Java代码自动生成中内存安全验证方法在说明书摘要公布了：本发明公开了一种基于Event‑B的Java代码自动生成中内存安全验证方法，首先明确内存管理系统的功能需求、环境需求和安全需求，然后对内存管理系统进行抽象建模，定义系统的核心功能，包括内存分配、回收和状态管理等，通过形式化描述内存管理过程，确保系统行为的可验证性，精化策略从初始抽象模型开始，逐步引入不同的功能需求和安全需求进行精化，在每一步精化过程中，均对模型进行验证；构建从Event‑B到JML，再到Java代码的安全转换规则，并使用IsabelleHOL定理证明器对系统行为的语义进行验证，确保了代码转换过程中内存操作的正确性，实现了从Event‑B模型到Java代码的安全转化。

本发明授权基于Event-B的Java代码自动生成中内存安全验证方法在权利要求书中公布了：1.一种基于Event-B的Java代码自动生成中内存安全验证方法，其特征在于，包括以下步骤：第一步，明确基于Event-B的Java代码自动生成中的内存管理系统的功能需求、环境需求和安全需求，其中：功能需求包括：动态内存分配与释放，内存合并与分割，内存状态追踪与管理；环境需求包括：适应不同设备硬件限制的抽象环境约束，内存隔离机制，指针操作模型的结构及其相关操作的指针约束与状态约束；安全需求包括：防止空指针解引用，防止内存泄漏，减少内存碎片；第二步，内存管理的Event-B建模：对内存管理系统进行抽象建模，定义系统的核心功能，包括内存分配与释放、合并与分割和状态追踪与管理，通过基于Event-B语言的形式化描述内存管理过程，确保系统行为的可验证性、正确性和一致性，精化策略从初始抽象模型开始，逐步引入不同的功能需求和安全需求进行精化，在每一步精化过程中，均对模型进行验证，确保新功能和属性的引入不会破坏已有的系统性质，直到最终获得包含全部功能、环境、安全需求的内存管理系统模型；第三步，将Event-B机器模型转换为JML语言，每个机器中的事件被分解为两个JML方法：一个用于检测守卫条件的guard方法和一个用于执行操作的run方法，JML方法通过不同的规范情况确保事件在满足条件时执行且保持状态一致，并通过存在量化符和谓词操作来精确表达Event-B中的赋值和状态变化，将形式化规范与Java实现紧密结合，并通过验证确保转换后的Java代码仍满足原始模型的安全约束；第四步，将Event-B的形式化机器模型转换为抽象的JML注释Java类，转换的类包含由Event-B事件转换而来的抽象方法，这些方法在Java中被继承和实现，确保每个步骤都符合内存管理系统的需求，并在转换过程中，对内存块状态的初始化和约束条件进行验证；其中，第三步和第四步中使用IsabelleHOL定理证明工具在Event-B机器模型到JML的转换，以及JML到Java的转换过程对内存管理系统行为的语义进行形式化验证，保证每个转换步骤中内存操作的可验证性、正确性和一致性，最终将Event-B机器模型转化为带有JML注释的Java代码，进而完成基于Event-B的内存管理Java代码自动生成。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人中铁第六勘察设计院集团有限公司;中国国家铁路集团有限公司，其通讯地址为：300450 天津市滨海新区自贸试验区(空港经济区)中环西路36号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。