PROMELA based formal verification for safety-critical software

Liang XING、Chengjun Ding、Hupeng DU、Chunyan Ma

2022Xibei Gongye Daxue Xuebao/Journal of Northwestern Polytechnical UniversityComputer Science被引 1开放获取

摘要

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

引用本文（GB/T 7714）

Liang XING, Chengjun Ding, Hupeng DU, 等. PROMELA based formal verification for safety-critical software[J]. Xibei Gongye Daxue Xuebao/Journal of Northwestern Polytechnical University, 2022.

引文网络

参考文献与被引分析加载中…

DOI：https://doi.org/10.1051/jnwpu/20224051180

本站仅收录题录与摘要供学习参考，全文版权归属出版方；如有侵权请联系我们删除。