随着航电软件在航电系统中的重要性的不断提高,设计和建立支持精确高效的航电软件需求形式化建模及其验证方法成为了当前提升航电系统安全性和开发效率的关键,也是满足适航标准形式化开发要求的必要保证。基于图形描述的建模语言Sys ML/MARTE是基于模型的软件工程（Model Based Software Engineering,MBSE）实践中采用的主流建模语言,常被应用于安全关键软件需求的规约。与自然语言相比,图形化的需求描述方式提升了需求的表达能力和可理解性,有利于研发效率的提升。但是,由于缺乏系统和严谨的语义定义,Sys ML/MARTE会给系统的开发带来精确性和一致性方面的问题,威胁安全关键软件的正确性。本文针对航电系统需求多层次、多源性和高复杂的特点,以表达能力、应用需要和保证安全为衡量标准,在抽取Sys ML和MARTE建模语言的安全子集基础上,结合安全自动机理论,构建了面向航电软件需求的安全建模语言Safety＿Sys ML安全状态机（Safety＿Sys ML State Machine,S2MSM）。本文的主要贡献包括:·提出了一个面向航电多层次需求的形式化建模语言S2MSM,该语言抽取Sys ML和MARTE建模语言的安全子集,并结合安全自动机理论,支持航电高层需求和低层需求的分析和验证。·构造了S2MSM的形式化语法和语义,使用标签迁移系统作为S2MSM的语义模型,构造了S2MSM中建模元和语义环境的形式化语义。该语言创新地融合了行为状态机和安全自动机的理论知识,构建了分层的语义,提升了开发过程中的精确性和一致性,并广泛适用于安全关键系统。·构造了从S2MSM高层需求模型到S2MSM低层需求模型的精化映射关系和精化映射规则。从结构和RTC语义的角度,对模型的精化映射进行分析,证明了S2MSM建模语言用于开发航电软件的可行性和正确性。·设计并实现了基于S2MSM的形式化建模工具S2M,以支持使用S2MSM对安全关键软件需求进行形式化建模与验证。为了展示方法的可行性和有效性,本文以飞机滚转角控制系统为例说明了S2MSM以及精化映射规则在航电系统中的具体应用。