一个基于形式化方法的系统安全性建模分析实例研究

石梦烨，胡 军，陈 朔，唐红英，王立松

(南京航空航天大学 计算机科学与技术学院，南京 211106)(软件新技术与产业化协同创新中心，南京 211106)

1 引 言

近年来，随着各类安全关键系统[1，2]功能的不断增强和需求的日益增加，对传统的系统工程开发和安全性分析技术提出了很大的挑战.基于模型的安全性分析[3，4](Model Based Safety Analysis，MBSA)是近年出现的一类对复杂系统建模并基于系统模型实现自动或半自动化的安全分析及验证的技术方法.MBSA已成为系统建模和分析领域的一个热点研究问题.

MBSA方法是形式化方法在安全关键系统的应用，旨在系统复杂性上升的同时保持或提高其安全性水平.它用于支持系统设计层级的分析，包括三个关键要素[5]：

1)对整个系统进行形式化模型的构建，其中模型是组件的集合；

2)对模型进行定性和定量分析，将可能存在的安全问题设置成一系列故障模式；

3)对扩展模型进行形式化安全分析.

国际汽车工程师协会(Society of Automotive Engineers，SAE)架构分析与设计语言(Architecture Analysis and Design Language，AADL)[6，7]是一种形式化建模语言，通过可扩展的标记符、工具框架和精确的语法语义，用于设计和分析复杂系统的软件和硬件架构及其性能关键特性.

本文主要工作以AADL的子集SLIM为建模语言，基于xSAP(The eXtended Safety Assessment Platform)为安全性分析平台的形式化验证方法[8]，以AIR6110中的机轮刹车系统[9]为实例，对其进行安全性建模和分析.通过一个实例展现了面向SLIM模型进行安全性分析和形式化验证的过程.本文的结构安排如下：第二节，主要介绍了MBSA框架、形式化方法在MBSA的应用、建模语言SLIM，和验证工具NuSMV[10，11]；……