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

PROMELA based formal verification for safety⁃critical software

作　　者：邢亮[1] 丁成钧 杜虎鹏 马春燕[2] XING Liang;DING Chengjun;DU Hupeng;MA Chunyan(Aeronautic Computing Technology Research Institute,Xi′an 710076,China;School of Software,Northwestern Polytechnical University,Xi′an 710072,China)

机构地区：[1]航空工业西安航空计算技术研究所,陕西西安710076 [2]西北工业大学软件学院,陕西西安710072

出　　处：《西北工业大学学报》2022年第5期1180-1187,共8页Journal of Northwestern Polytechnical University

基　　金：航空科学基金(20185853038,201907053004)资助。

摘　　要：聚焦安全关键软件,研究基于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.

关 键 词：C程序 PROMELA模型 软件故障 形式化验证 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]