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

作者简介:

魏晓敏(1990-), 男, 博士, 讲师, CCF专业会员, 主要研究领域为系统安全, 形式化验证, 嵌入式软件, 无人机系统. ;董云卫(1968-), 男, 博士, 教授, 博士生导师, CCF杰出会员, 主要研究领域为嵌入式系统, 模型驱动开发方法, 信息-物理融合系统, 软件测试. ;孙聪(1982-), 男, 博士, 教授, 博士生导师, CCF专业会员, 主要研究领域为信息流分析, 可信软件, 程序分析与验证, 无人系统安全. ;李兴华(1978-), 男, 博士, 教授, 博士生导师, CCF专业会员, 主要研究领域为云计算安全, 攻击检测, 数据安全, 隐私保护, 无线网络安全;马建峰(1963-), 男, 博士, 教授, 博士生导师, CCF会士, 主要研究领域为应用密码学, 无线网络安全, 数据安全, 移动智能系统安全.

通讯作者:

董云卫, E-mail: yunweidong@nwpu.edu.cn

中图分类号:

基金项目:

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


Safety Analysis for Mixed-criticality System with Random Errors and Burst Errors Based on AADL
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    Many complex embedded systems are mixed-criticality systems (MCSs). MCSs are often required to operate with the specified criticality level, but they may be subject to hazards that can induce random errors and burst errors, which may result in the abortion of an executing thread or even system failures. Current research only concentrates on schedulability analysis for MCSs and fails to further analyze system safety and consider the dependency relationship among threads. Taking random errors and burst errors as the research objects, this study proposes an architecture-based MCS safety analysis method with the integration of fault propagation analysis. Meanwhile, architecture analysis and design language (AADL) is employed to characterize the dependency relations among components. To compensate for the shortcomings of AADL, this study creates new AADL properties (AADL burst error properties) and proposes new thread state machine (burst error-based thread state machine) semantics to describe the thread execution process with burst errors. Additionally, model transformation rules and assembly methods are proposed to apply probabilistic model checking for safety analysis, and PRISM models are derived from AADL models. Two formulae are also formulated to obtain quantitative safety properties for verifying occurrence probabilities of failures, and qualitative safety properties for generating corresponding witnesses to figure out propagation paths for fault propagation analysis respectively. Finally, the effectiveness of the proposed method is verified by adopting a power boat autopilot (PBA) system.

    参考文献
    相似文献
    引证文献
引用本文

魏晓敏,董云卫,孙聪,李兴华,马建峰.基于AADL的混合关键系统随机错误与突发错误安全性分析.软件学报,2024,35(9):4287-4309

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2023-09-11
  • 最后修改日期:2023-10-30
  • 录用日期:
  • 在线发布日期: 2024-01-05
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号