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

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