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

Liang Xing, Chengjun Ding, Hupeng Du, Chunyan Ma

科研成果: 期刊稿件文章同行评审

摘要

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.

投稿的翻译标题PROMELA based formal verification for safety-critical software
源语言繁体中文
页(从-至)1180-1187
页数8
期刊Xibei Gongye Daxue Xuebao/Journal of Northwestern Polytechnical University
40
5
DOI
出版状态已出版 - 10月 2022

关键词

  • C program
  • formal verification
  • PROMELA model
  • software failure

指纹

探究 '基于 PROMELA 模型的安全关键软件形式化验证技术' 的科研主题。它们共同构成独一无二的指纹。

引用此