利用特征配置的SLIM安全性验证方法

• 作者: 李宙洲 魏欧 黄鸣宇
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 安全关键系统 SLIM语言 fPromela语言 安全性验证 模型检测
• 年，卷（期）: 2017,（10）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 2346-2351
• 页数: 6页
• 分类号: TP311
• 字数: 6706字
• 语种: 中文

摘要

安全关键系统的愈发复杂,使得系统的安全性和开发成本面临着越来越大的挑战.由ESA赞助的COMPASS项目,使用SLIM对诸如航天器系统这样的安全关键系统进行建模,不仅可以描述系统标定的软硬件行为,还可以描述系统的概率性故障、故障对系统的影响和系统恢复.本文从软件产品线角度提出一个新颖的、针对SLIM扩展模型的验证方法—将软件产品线中产品的可变性引入安全性验证过程,将系统中的故障看作系统中可以进行配置的特征,直观、清楚地刻画了安全分析中系统的结构和行为.使用成熟的SLIM语言建立安全关键系统的扩展模型,将SLIM扩展模型中的故障作为特征、完成扩展模型到fPromela模型的转换;利用软件产品线模型检测工具SNIP对转换得到的fPromela模型进行检测,找出造成系统失效的故障,完成对SLIM扩展模型的安全性验证工作.根据模型转换的规则,设计并实现了转换工具S2F.同时,结合COMPASS给定的标准案例—数据采集系统进行实例分析.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	魏欧	南京航空航天大学计算机科学与技术学院	31	153	7.0	11.0
2	李宙洲	南京航空航天大学计算机科学与技术学院	2	2	1.0	1.0
3	黄鸣宇	南京航空航天大学计算机科学与技术学院	9	37	4.0	5.0