PROMELA based formal verification for safety-critical software

基于PROMELA模型的安全关键软件形式化验证技术

¹ Aeronautic Computing Technology Research Institute, Xi'an 710076, China
² School of Software, Northwestern Polytechnical University, Xi’an 710072, China

Received: 15 November 2021

Abstract

聚焦安全关键软件, 研究基于PROMELA形式模型验证C程序中违反断言、数组越界、空指针解引用、死锁及饥饿等5类故障技术。建立C程序抽象语法树节点到PROMELA模型, 验证属性相关函数到PROMELA模型的2类映射规则; 根据映射规则提出由C程序自动生成PROMELA形式模型的算法, 并对算法进行理论分析; 针对C程序中5种故障类型, 分别给出基于PROMELA模型的形式化验证方法, 并分析验证的范围; 覆盖各类故障的验证范围, 为每类故障类型选取12个C程序案例进行实证研究, 实验结果证明了方法的有效性。

摘要

Based on the PROMELA formal model, this paper studies the techniques for verifying the five types of fault in the C program: assertion violation, array out-of-bound, null pointer dereference, deadlock and starvation. Firstly, it establishes two types of mapping rules from the abstract syntax tree nodes of the C program to the PROMELA model and verifies the attribute-related functions of the PROMELA model. Secondly, according to the mapping rules, the algorithm for automatically generating the PROMELA formal model from the C program is proposed and theoretically analyzed. Then, based on the PROMELA model, the formal verification technique for the five types of fault in the C program respectively is given. Finally, the verification scope of the five types of fault is analyzed. For each type of fault, 12 cases of the C programs are studied. The experimental results demonstrate the effectiveness of the technique.