基于Event-B的Java代码自动生成中内存安全验证方法

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