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

龙图腾网获悉安徽大学申请的专利一种操作系统内核复杂数据结构形式化验证方法获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN116521539B 。

龙图腾网通过国家知识产权局官网在2025-12-12发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202310457374.5，技术领域涉及：G06F11/3604；该发明授权一种操作系统内核复杂数据结构形式化验证方法是由李薛剑;王俊宜设计研发完成，并于2023-04-25向国家知识产权局提交的专利申请。

本一种操作系统内核复杂数据结构形式化验证方法在说明书摘要公布了：本发明提供一种操作系统内核复杂数据结构形式化验证方法，首先基于块内存在操作上的定义，将内核中源程序对数据结构的操作映射到抽象内存中，将包含于程序层面数据结构对象的类型、字节大小等信息携带到内存模型中，得到对应抽象内存层面的性质；再依据基于内存状态语义的推理规则，得到内存操作过程中不同状态的断言；结合对抽象程序层定义的符合复杂结构描述语义模型的处理，得到经过扩展的霍尔逻辑，并通过符号化的程序逻辑进行推理；然后将逻辑推理和内存状态断言交由自动证明器进行证明，自动化验证复杂数据结构的相关性质是否满足期望。本发明实现了对操作系统内核复杂数据结构的高效、精确的形式化验证。

本发明授权一种操作系统内核复杂数据结构形式化验证方法在权利要求书中公布了：1.一种操作系统内核复杂数据结构形式化验证方法，其特征在于，包括以下步骤： S1、以内存块为基础建立内存模型：将复杂数据结构的操作进行函数形式的定义和描述，使程序层面的数据和结构操作映射到抽象的物理内存上； 所述内存模型具体通过以下方法建立： S11、确定内存块，将内存划分为不同的块来描述内存对象和操作，并定义基本数据类型，进行形式化的刻画和表示； S12、建立内存操作，将程序中所有数据和结构的操作映射到抽象的物理内存上，并以未解释函数的形式对内存块上的基本操作进行定义和描述，标识某一内存块的具体状态； S2、基于内存模型，形式化定义和描述内存对象操作性质，建立基于内存状态语义的推理规则，得到内存操作过程中不同状态的断言； S3、在程序层面对抽象的内存和内存块的状态进行描述，通过定义符合复杂结构描述的文法和语义建立语义模型； S4、基于语义模型得到扩展的霍尔逻辑，并通过符号化的程序逻辑进行推理，得到扩展的霍尔逻辑推理； S5、建立内存模型到程序语义的映射，将语义模型应用于基于内存操作的推理规则上，并建立高层程序层和低层抽象内存层之间的一致性关系：将高层关于复杂数据结构操作的推理和证明对应和映射到低层的内存空间的操作上，对数据结构对象和具体内存对象的操作建立映射关系； 所述建立高层程序层和低层抽象内存层之间的一致性关系具体包括以下步骤： S51、定义抽象内存的抽象程序的语义，说明一个满足给定抽象程序的内存状态； S52、根据程序语法，在内存模型定义和描述的基础上对程序语义进行定义和逻辑推理；将特定的程序文法对应到各自的具体内存空间上去进行判值，然后形成关于抽象内存空间的公理化推理规则； S53、在内存模型具体语义的基础上，在抽象内存层上对程序进行基于逻辑的推理规则的定义和说明； S54、对基本的霍尔式的逻辑推理进行扩展定义，得到基于内存模型描述的程序进行形式化的推断； S6、结合抽象内存层的断言以及扩展的霍尔逻辑推理，在具体内存的操作性质上进行验证：将内存状态断言和扩展的霍尔逻辑推理交给自动定理证明器进行证明，验证复杂数据结构的性质是否满足期望。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人安徽大学，其通讯地址为：230601 安徽省合肥市经济技术开发区九龙路111号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。

以上内容由龙图腾AI智能生成。