随着计算机的诞生及快速发展,其在各行业、各领域得到广泛应用,在安全关键系统中起着举足轻重的作用。对于安全关键系统而言,计算机的偶发故障或系统失效常常会带来危及生命、财产的重大损失。因此对安全关键系统,如飞机机载系统的安全性分析至关重要,不仅需要保证系统的正常功能行为是否完备,还需要在系统的需求分析及模型设计过程中充分的考虑可能的系统功能失效影响和处理故障的方式。形式化方法是一类基于逻辑形式语言的数学建模与分析方法,能够用于安全关键系统的建模、分析与验证,提高安全关键系统的安全性。针对航空安全关键系统需求的安全性,本文展开了一种基于形式化方法的系统需求建模与分析研究,具体包括以下几个方面:(1)设计了一个基于四变量模型的面向需求的建模与安全性分析框架。在这个框架中根据安全关键系统的需求规约的重要性,基于四变量模型思想对系统进行分析,采用基于四变量模型的形式化表格语言SCR对系统进行需求建模,验证SCR模型的需求完整性,并将整套思想运用在飞行引导系统的建模与需求完整性分析中;根据系统需求规约、模型转换和模型检验的思想,提出了一套基于NuSMV模型检验的需求验证框架;能够基于MBSA思想,对系统进行故障行为设计以及故障分析等。(2)提出了一套将SCR模型转换为NuSMV模型的转换方法。由于基于四变量模型的SCR模型仅能验证系统需求的完备性,不能够检验系统功能性属性,因此需要将其转换为可以进行功能性属性验证的NuSMV模型。本文研究了SCR语言与NuSMV语言的语法语义及其特征,提出了两种语言间的模型转换方法,能够保证语义一致性,包括类型与变量的转换、时态间的对应以及SCR语言中模式及项到NuSMV语言中子模块的转换等。(3)建立了基于故障注入机制及模型扩展思想的系统验证与安全性分析过程。该过程包括根据系统行为特征设计系统故障行为,对系统正常行为模型进行故障注入,识别系统顶事件,对系统正常行为模型进行模型扩展得到故障扩展模型以及进行故障分析等。(4)针对一个真实的综合航电系统进行了需求建模及安全性的实例分析。包括分析飞行引导系统的架构特征,特别是其所包含的模式逻辑;基于四变量模型思想对该实例系统进行了需求分析,使用SCR语言对其进行需求建模,并进行需求完整性分析;将SCR模型转换为NuSMV模型,验证系统功能性属性的正确性;构造多种故障模式对实例系统进行故障分析,生成故障树和FMEA表等。