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

来源：计算机技术与发展杂志2024年第08期北京时间：

作者：李薛剑;王俊宜

摘要：对系统中操作复杂结构程序的正确性验证是保证软件高可信的重要途径,目前大多数基于高层抽象建模和程序结构拆分的方法难以满足复杂数据结构程序的验证要求。 针对这一问题,论文提出基于类 C 语言内存模型的验证方法。首先,以内存块为基础将复杂数据结构的操作进行函数形式的定义和描述,形式化描述内存对象操作性质;其次,针对程序层定义了符合复杂结构描述的文法和语义,并基于符号化的程序逻辑进行推理。 实验对嵌入式操作系统内核 滋C/ OS?III 中的复杂数据结构进行分析和自动化验证,断言描述和验证条件脚本通过了自动定理证明器的求解。

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