航电系统是一种可靠性要求度极高的安全关键系统,形式化验证将贯穿在航电系统中的每个生命周期阶段。在工业界,EA由于其具有普适性被广泛应用在各个领域的模型构建中。而在航电领域,AADL由于其出色的航空体系架构能力而被广泛应用。如何提高EA的形式化验证能力和航电系统的体系架构分析能力,是一个待以解决的问题。针对航电系统的特点和需求,本文提出的工具链是一类模型转化器,包含Safety＿SysML和EA2AADL两部分,旨在将Safety＿SysML模型转化为EA模型再转化为AADL模型。本文的主要贡献包括:研究不同平台之间模型转化的方法。通过研究和制定各平台的模型约束文件,从而生成模型的接口或类文件。然后结合制定的一系列模型映射集以实现不同平台之间模型转化的功能。设计并实现了Safety＿SysML2EA模型转化工具。Safety＿SysML2EA是以Safety＿SysML为主要形式化建模语言,以安全自动状态机为载体,以MDA为主要理论依据,把校验成功后的安全自动状态机模型转换到EA模型的工具。将Safety＿SysML2EA转化工具与S2M验证链集成。在模型转化过程中,本文集成了S2M模型验证器以实现对状态机的安全性校验。根据不同的验证目的和顺序,本文提出了命令链的方式进行校验。设计并实现EA2AADL模型转化工具。EA2AADL是以EA平台上的SysML块图（BDD/IBD）和状态图作为输入,以AADL模型为输出的模型转化工具,旨在将EA模型转化为AADL模型。其转化思想和逻辑与Safety＿SysML2EA工具类似。为了展示转化工具的正确性,本文以飞机制导系统作为案例来说明Safety＿SysML2EA和EA2AADL模型转化工具在航电系统中的具体应用。