基于AADL的混合关键系统随机错误与突发错误安全性分析

作     者：魏晓敏 董云卫 孙聪 李兴华 马建峰 

作者机构：西北工业大学计算机学院 西安电子科技大学网络与信息安全学院 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2024年

核心收录：

学科分类：08[工学] 082402[工学-轮机工程] 0824[工学-船舶与海洋工程] 082401[工学-船舶与海洋结构物设计制造] 

基　　金：国家自然科学基金(62232013,62272366,62125205) 中央高校基本科研业务费专项资金(ZYTS23165) 陕西省重点研发计划(2023-YBGY-371) 

主　　题：混合关键系统 突发错误 模型转换 安全性分析 概率模型检验 

摘      要：许多复杂的嵌入式系统都是混合关键系统(mixed-criticality system, MCS). MCS通常需要在指定的关键性(criticality)等级状态下运行,但是它们可能会受到一些危害的影响,这些危害可能会导致随机错误和突发错误,进一步导致执行线程中止,甚至导致系统故障.目前的研究仅集中于对MCS的可调度性分析,未能进一步分析系统安全性,未能考虑线程之间的依赖关系.以随机错误和突发错误为研究对象,提出一种集成故障传播分析的基于架构的MCS安全分析方法.使用架构分析和设计语言(architecture analysis and design language, AADL)刻画构件依赖关系.为了弥补AADL的不足,创建新的AADL属性(AADL突发错误属性),并提出新的线程状态机(突发错误行为线程状态机)语义来描述带有突发错误的线程执行过程.为了将概率模型检查应用于安全分析,提出模型转换规则和组装方法,从AADL模型推导出PRISM模型.建立了两个公式,分别获得定量安全属性以验证故障发生的概率,以及定性安全属性以生成相应的正例来求出故障传播路径来进行故障传播分析.最后,以动力艇自动驾驶仪(power boat autopilot, PBA)系统为例,验证了该方法的有效性.