一种基于操作表达式模型的关键软件安全性验证方法研究

A Approach for Critical Software Safety Verification Based on Operation Expression Model

目前在安全关键领域,软件系统的安全性分析与验证已经成为软件工程研究中的热点问题,本文工作给出一种基于镜像理论中操作表达式模型的关键软件安全性的验证方法.设计了从操作表达式模型到其分析树的自动转换方法;采用镜像理论的语义公理、定理及计算规则对分析树节点进行语义谓词计算,从而得到完整的附有语义谓词的语义树;使用镜像理论的定理证明规则验证语义树中各节点需要满足的安全性质规约;还给出了相应的原型工具和验证实例分析;此方法已在航空航天领域得到实际应用.

In the field of safety critical,software systems analysis and verification has become a very important hotspot in the software engineering research. This paper is based on the Mirror Theory,and give a safety verification method. Specially,the analysis tree is created based on the operation expression,and then the semantic predicate of each node in the tree is generated by the semantic axioms,theorems and some calculated rules. Secondly,the result of programs safety is obtained by verifying the corresponding specification with the logic of Mirror Theory. Finally,a tool and example are given to demonstrate its value,and this approach has been applied in the aerospace and astronautics field.