陈 朔，胡 军，王立松

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

1 引 言

目前随着工业系统的规模不断增加，系统故障往往会引起重大的生命和财产损失[1]，因此安全关键系统的安全性和可靠性分析就显得尤为重要.但是传统系统工程无法很好的解决复杂安全关键系统的模型构建和分析问题[2]，基于MBSA(Model-Based safety assessment)的安全关键系统分析方法在近些年来逐步受到业界的广泛关注[3].MBSA的核心是首先对整个系统进行模型构建，然后通过对整个模型的定性和定量分析，来发现模型中可能存在的安全缺陷和潜在的系统风险.MBSA通过在系统模型设计层级进行安全分析，消除这些风险可能导致的后果，提高整个系统的安全性[4].

AltaRica 3.0[5-7]是一种基于MBSA的多层次的模型语言，并结合形式化方法对系统的安全性进行分析，目前在航空航天系统安全分析领域有着较为广泛的应用.AltaRica 3.0模型中的层次结构S2ML是用来描述真实系统的复杂层次架构和相应系统中部件的关联信息，而要对AltaRica 3.0模型进行安全性验证，就要将AltaRica 3.0模型的层次结构转换成形式化语义模型，AltaRica 3.0的形式化语义模型是一类卫士转换系统GTS(Guarded Transition Systems)[8]，由于GTS所具有的的形式化语义特征，就可以应用马尔可夫生成器[9]、随机仿真、模型检测等工具进行对AltaRica 3.0模型进行有效的安全性分析与验证.因此，将AltaRica 3.0的层次模型(S2ML)转换为语义等价的平展化模型(GTS)是进行系统安全分析的一个关键步骤.

本文的主要研究内容如下：第2节介绍本文的相关工作和国内外研究现状；……