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

小 型 微 型 计 算 机 系 统Journal of Chinese Computer Systems2014 年 7 月 第 7 期Vol． 35 No． 7 2014一种基于操作表达式模型的关键软件安全性验证方法研究曲长亮1 ，胡军1，2 ，徐丙凤1 ，黄志球11 ( 南京航空航天大学 计算机科学与技术学院，南京 210016)2 ( 南京大学 计算机软件新技术国家重点实验室，南京 210093)mail:qcl_nuaa@ nuaa． edu． cn摘 要: 目前在安全关键领域，软件系统的安全性分析与验证已经成为软件工程研究中的热点问题，本文工作给出一种基于镜 像理论中操作表达式模型的关键软件安全性的验证方法． 设计了从操作表达式模型到其分析树的自动转换方法;采用镜像理论 的语义公理、定理及计算规则对分析树节点进行语义谓词计算，从而得到完整的附有语义谓词的语义树;使用镜像理论的定理 证明规则验证语义树中各节点需要满足的安全性质规约;还给出了相应的原型工具和验证实例分析;此方法已在航空航天领域 得到实际应用．关 键 词: 软件分析;安全性验证;操作表达式;镜像理论;语义树中图分类号: TP311文献标识码:A文 章 编 号:1000-1220(2014)07-1578-07A Approach for Critical Software Safety Verification Based on Operation Expression ModelQU Chang-liang1 ，HUJun1，2 ，XU Bing-feng1 ，HUANG Zhi-qiu11 ( College of Computer Science and Technology ，Nanjing University of Aeronautics and Astronautics，Nanjing 210016，China)2 ( State Key Laboratory for Novel Software Technology ，Nanjing University，Nanjing 210093，China)Abstract:In the field of safety critical，softw are 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 axi- oms，theorems and some calculated rules． Secondly，the result of programs safety is obtained by verifying the corresponding specifica- tion 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．Key words:software analysis;safety verification;operation expression( OE);mirror theory;senmatic tree1引言随着计算机技术的发展，计算机软件已经广泛地应用到 社会的各个方面，与此同时软件系统的结构越来越复杂，规模 也越来越大，对系统的安全性要求也越来越高，在航空航天、 核电和铁路各领域尤为显著，一旦软件发生故障将可能带来 无可估量的生命和财产损失． 例如:2010 年 8 月，由于软件故 障，导致美国海军所属的一架无人直升机在失去控制后闯进 了华盛顿上空的禁飞区［1］ 等． 因此，对安全关键领域中的软 件安全性分析与验证已成为现代软件工程中研究热点．镜像理论［2］是由北京大学袁崇