期刊论文

Safety Verification Methods for SLIM Using Features Configuration

中文

小型微型计算机系统

Journal of Chinese Computer Systems

0513-353X

2017

30

10

2346-2351

国家“九七三”重点基础研究发展计划项目(2014CB744904)资助； 国家自然科学基金项目(61170043)资助； 航空科学基金项目(20155552047)资助；

本校为其他机构

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

With the complex of safety-critical system is enhanced, the safety and development costs of the system are facing great challenges. The COMPASS project sponsored by ESA （ Europe Space Agency）, adopts SLIM to model the safety-critical system such as aerospace system, which can describe not only nominal hardware and software operations, but also probabilistic faults and their propagation and recovery. From the perspective of software product line ,this paper provides a novel verification method applicable to SLIM expended model… introduce the ...