基于形式化测试的实时系统变更后安全性验证

孙海英; 刘静; 陈小红; 杜德慧; 周庭梁

首页> 中文期刊> 《中国科学：信息科学》 >基于形式化测试的实时系统变更后安全性验证

基于形式化测试的实时系统变更后安全性验证

开具论文收录证明 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

变更后系统实现的安全性验证是安全攸关系统维护过程中必不可少的环节,也是其面临的主要挑战之一.软件模型检测和程序验证是目前常用的作用于代码层面的自动化安全性验证技术.本文站在系统行为角度,基于形式化方法,提出了一种将变更后系统实现的安全性验证问题归结为一致性测试的方法,尝试通过自动生成的一致性测试用例在系统行为级别上判定系统实现是否安全.为此,首先以时间输入输出自动机及其语义模型为基础,构建了该方法的证明体系,证明了该方法的正确性;其次,建立了变更后系统实现安全性验证的回归测试生成框架.相对于其它实时系统测试方法,这种测试方法不仅可以发现实时系统中常规的不一致性缺陷,而且为变更后系统实现在运行时是否满足指定的安全性属性提供了依据.最后,以轨道交通系统中的列车自动防护功能的变更情景为案例研究,说明了方法的具体应用.

著录项

来源
《中国科学：信息科学》 |2014年第1期|70-90|共21页
作者
孙海英; 刘静; 陈小红; 杜德慧; 周庭梁;
展开▼
作者单位

华东师范大学;

上海市高可信重点实验室;

上海200062;

同济大学道路与交通工程教育部重点实验室;

上海200092;

展开▼
原文格式 PDF
正文语种 chi
中图分类 TP311.52;
关键词
软件工程; 软件演化; 实时系统; 形式化方法; 安全性验证; 软件测试; 安全性测试;

相似文献

中文文献
外文文献
专利

1. 一种基于时间自动机网络的实时系统形式化验证方法 [J] . 刘传会 ,张广泉 . 苏州大学学报（自然科学版） . 2008,第001期
2. 基于验证法的对某颤振实时系统故障测试研究 [J] . 高培先 . 计算机测量与控制 . 2009,第011期
3. 基于CC的安全性规格形式化描述及验证方法 [J] . 闫靖晨 ,程京德 . 信息安全研究 . 2017,第007期
4. 基于CC的安全性规格形式化描述及验证方法 [J] . 闫靖晨 ,程京德 . 信息安全研究 . 2017,第007期
5. 基于形式化单子的第三方构件安全性测试模型及其应用 [J] . 陈锦富 ,赵小磊 ,刘一松 . 计算机学报 . 2019,第007期
6. 基于形式化方法的软件安全性验证技术研究 [C] . 经小川 ,张刚 . 全国软件测试能力验证总结会暨中国宇航学会计算机应用专业委员会2006年学术年会 . 2006
7. 基于模型的实时系统形式化验证方法研究与实现 [A] . 冯博洋 . 2016

基于形式化测试的实时系统变更后安全性验证

摘要

著录项

相似文献

相关主题

期刊订阅