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

• 作者: 徐丙凤 曲长亮 胡军 黄志球
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 软件分析 安全性验证 操作表达式 镜像理论 语义树
• 年，卷（期）: 2014,（7）
• 所属期刊栏目: 计算机软件与数据库技术
• 页码范围: 1578-1584
• 页数: 7页
• 分类号: TP311
• 字数: 7767字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术学院	183	1755	20.0	33.0
2	胡军	南京航空航天大学计算机科学与技术学院	41	358	10.0	18.0
6	徐丙凤	南京航空航天大学计算机科学与技术学院	16	297	9.0	16.0
7	曲长亮	南京航空航天大学计算机科学与技术学院	2	18	2.0	2.0