[1]李薛剑,王俊宜.基于类C语言内存模型的复杂数据结构验证方法[J].计算机技术与发展,2024,34(08):57-66.[doi:10.20165/j.cnki.ISSN1673-629X.2024.0134]
　LI Xue-jian,WANG Jun-yi.C-like Memory Model Based Verification Method for Complex Data Structures[J].,2024,34(08):57-66.[doi:10.20165/j.cnki.ISSN1673-629X.2024.0134]
点击复制

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

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
34
期数:
2024年08期
页码:
57-66
栏目:
软件技术与工程
出版日期:
2024-08-10

文章信息/Info

Title:
C-like Memory Model Based Verification Method for Complex Data Structures
文章编号:
1673-629X(2024)08-0057-10
作者:
李薛剑; 王俊宜
安徽大学 计算机科学与技术学院,安徽 合肥 230601
Author(s):
LI Xue-jian; WANG Jun-yi
School of Computer Science and Technology,Anhui University,Hefei 230601,China
关键词:
形式化验证; 复杂数据结构; 程序逻辑; 内存模型; 操作系统内核
Keywords:
formal verification; complex data structures; program logic; memory model; operating system kernel
分类号:
TP301.2
DOI:
10.20165/j.cnki.ISSN1673-629X.2024.0134
摘要:
对系统中操作复杂结构程序的正确性验证是保证软件高可信的重要途径,目前大多数基于高层抽象建模和程序 结构拆分的方法难以满足复杂数据结构程序的验证要求。 针对这一问题,论文提出基于类 C 语言内存模型的验证方法。首先,以内存块为基础将复杂数据结构的操作进行函数形式的定义和描述,形式化描述内存对象操作性质;其次,针对程序层定义了符合复杂结构描述的文法和语义,并基于符号化的程序逻辑进行推理。 实验对嵌入式操作系统内核 滋C/ OS?III 中的复杂数据结构进行分析和自动化验证,断言描述和验证条件脚本通过了自动定理证明器的求解。
Abstract:
Verification of complex data structures in the operating system kernel is an important approach to ensure high confidence of software. In order to verify the correctness of programs operating complex structures in the system,most recent methods based on high-level abstraction 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.

相似文献/References:

[1]黄吴丹,严俊琦.路由协议的自动形式化验证方法研究[J].计算机技术与发展,2017,27(12):1.
　HUANG Wu-dan,YAN Jun-qi.Research on Automated Formal Verification of Routing Protocols[J].,2017,27(08):1.
[2]司 佳,朱羿全,马 琳.基于时序描述逻辑的故障树分析方法研究[J].计算机技术与发展,2017,27(12):89.[doi:10.3969/ j. issn.1673-629X.2017.12.020]
　SI Jia,ZHU Yi-quan,MA Lin.Research on Fault Tree Analysis Based on Temporal Description Logic[J].,2017,27(08):89.[doi:10.3969/ j. issn.1673-629X.2017.12.020]
[3]邓刘梦,葛晓瑜,宛伟健.基于 NuSMV 的 SysML 模型形式化验证[J].计算机技术与发展,2019,29(10):153.[doi:10. 3969 / j. issn. 1673-629X. 2019. 10. 030]
　DENG Liu-meng,GE Xiao-yu,WAN Wei-jian.Formal Verification of SysML Model Based on NuSMV[J].,2019,29(08):153.[doi:10. 3969 / j. issn. 1673-629X. 2019. 10. 030]
[4]王赫彬,郑长友,黄摇 松,等.以太坊智能合约安全形式化验证方法研究进展[J].计算机技术与发展,2021,31(09):104.[doi:10. 3969 / j. issn. 1673-629X. 2021. 09. 018]
　WANG He-bin,ZHENG Chang-you,HUANG Song,et al.Review:Secure Formal Verification Methods for Ethereum Smart Contracts[J].,2021,31(08):104.[doi:10. 3969 / j. issn. 1673-629X. 2021. 09. 018]
[5]方雨瑶,张 聪.基于多引擎并行协作的 SCADE 模型检测[J].计算机技术与发展,2023,33(11):86.[doi:10. 3969 / j. issn. 1673-629X. 2023. 11. 013]
　FANG Yu-yao,ZHANG Cong.SCADE Model Checking Based on Multi-engine Parallel Collaboration[J].,2023,33(08):86.[doi:10. 3969 / j. issn. 1673-629X. 2023. 11. 013]

更新日期/Last Update: 2024-08-10