随着航空、交通、医疗等安全关键系统的规模越来越大,如何提高复杂关键安全系统的安全性,防止重大人员伤亡,成为急需解决的问题。传统建模方式所创建的模型和实际的系统差别很大,模型不能在整个开发设计过程中使用。规范中很小的变动就可能导致重新遍历所有安全模型,容易出错也消耗资源。高级别建模语言AltaRica的提出解决了这一问题,AltaRica模型是一种组件可重用的层次结构,由法国工业和学术协会专门为工业系统的安全评估所设计的一门MBSA建模语言。随着AltaRica3.0的更新,ARC等传统的AltaRica建模分析工具已不再支持,而SPIN作为一个穷尽式模型验证工具被广泛应用。由于SPIN不能直接用来对AltaRica3.0模型分析和验证,因此需要将AltaRica3.0模型转换为Promela模型。针对上述问题,本文的主要工作是提出了来一种基于Simfia图形化建模,转换为AltaRica3.0模型,继而转换为Promela模型,随后使用SPIN工具验证的一套从建模到转换到验证的方法。具体工作如下所示:(1)提出了基于Simfia的AltaRica3.0建模方法,并使用飞机的显示控制系统为例建模并分析其故障树。首先介绍了AltaRica3.0和Simfia的基本知识,分析了AltaRica3.0和Simfia模型的特点;提出了基于Simfia的AltaRica3.0模型的建模方法,指出了Simfia模型元素和AltaRica3.0模型元素之间的映射关系;最后以飞机的显示控制系统为例,为其建立了Simfia模型,并转换为了AltaRica3.0模型,使用故障树分析软件对其故障树做了简要分析。(2)分析了AltaRica3.0模型扁平化为GTS模型的具体方法,并吸取其思想提出了AltaRica3.0模型转换为Promela模型的详细方法。首先分析了AltaRica3.0扁平化为GTS模型的详细规则;分析了AltaRica3.0和Promela的语义模型;根据扁平化思想提出了AltaRica3.0模型转换为Promela模型的详细规则,并验证了其可行性;最后以简单供水系统为例说明了AltaRica3.0模型转换为Promela模型的步骤。(3)以飞机的机轮刹车系统为例,为其建立了AltaRica3.0模型,并转换为Promela模型进行分析和验证。以飞机的机轮刹车系统为例,对其建立AltaRica3.0模型,使用Arbre Analyste对其故障树进行分析;将其转换为Promela模型使用SPIN分析和验证,通过综合两种分析方式得出的结论对系统进行评估,并给出修改意见。