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

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.