基于类C语言内存模型的复杂数据结构验证方法  

C-like Memory Model Based Verification Method for Complex Data Structures

作　　者：李薛剑[1] 王俊宜 LI Xue-jian;WANG Jun-yi(School of Computer Science and Technology,Anhui University,Hefei 230601,China)

机构地区：[1]安徽大学计算机科学与技术学院,安徽合肥230601

出　　处：《计算机技术与发展》2024年第8期57-66,共10页Computer Technology and Development

基　　金：安徽省自然科学基金面上项目(2008085MF188)。

摘　　要：对系统中操作复杂结构程序的正确性验证是保证软件高可信的重要途径,目前大多数基于高层抽象建模和程序结构拆分的方法难以满足复杂数据结构程序的验证要求。针对这一问题,论文提出基于类C语言内存模型的验证方法。首先,以内存块为基础将复杂数据结构的操作进行函数形式的定义和描述,形式化描述内存对象操作性质;其次,针对程序层定义了符合复杂结构描述的文法和语义,并基于符号化的程序逻辑进行推理。实验对嵌入式操作系统内核μC/OS-III中的复杂数据结构进行分析和自动化验证,断言描述和验证条件脚本通过了自动定理证明器的求解。ion modeling and program structure decomposition struggle to meet the verification requirements of programs with complex data structures.In response to this problem,we propose a verification method based on the C-like memory model.First,based on memory blocks,complex data structure operations are defined and described in the form of functions,providing a formal description of the operational properties of memory objects.Second,grammar and semantics that conform to the description of complex structures are defined at the program level,and reasoning is conducted based on symbolic program logic.Experimental analysis and automated verification were conducted on complex data structures within the embedded operating system kernel ofμC/OS-III,assertions and verification condition scripts were solved using an automated theorem prover.

关 键 词：形式化验证 复杂数据结构 程序逻辑 内存模型 操作系统内核 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]