Xibei Gongye Daxue Xuebao (Oct 2022)

PROMELA based formal verification for safety-critical software

  • XING Liang,
  • DING Chengjun,
  • DU Hupeng,
  • MA Chunyan

DOI
https://doi.org/10.1051/jnwpu/20224051180
Journal volume & issue
Vol. 40, no. 5
pp. 1180 – 1187

Abstract

Read online

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

Keywords