買專利賣專利找龍圖騰，真高效！ 查專利查商標用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或微信搜索“龍圖騰網”。