随着系统设计越来越复杂,自动化程度越来越高,判断系统行为安全与否的难度也越来越大。因此,安全性验证在工程领域备受重视,民机的飞行安全验证也是学术界与工程界的研究热点。影响飞行安全的因素很多,包括机体、飞行环境、意外因素、人为因素等。据统计,民用飞机事故的75％以上是由于飞行员的操作失误、疏忽或判断失误等。所以,在考虑人为因素的前提下,寻找验证民机飞行安全的有效方法十分必要。　　一般用于验证的仿真方法每次只能模拟单一轨迹,对于有多输入、多状态的复杂系统来说,对可能的轨迹进行逐条分析的代价过高,不易实现。后向可达集能够通过单次仿真捕获所有轨迹演化集合,是验证系统安全性的有效方法。根据给定系统的物理模型和目标状态集,所有能够在一定时间段内到达目标集的轨迹集合就是所要计算的后向可达集。如果目标集为安全状态集合,那么后向可达集所包含的状态也是安全的。因此,所求得的后向可达集可用作飞行安全性验证的判据。　　本文后向可达集的计算是基于时间依赖的Hamilton-Jacobi偏微分方程(简称HJ PDE),此偏微分方程粘性解的零子水平集可以作为给定时间段内的后向可达集的隐式表达。本文将此可达集计算方法分别应用于理想的飞行纵向模型和简化的6自由度人在环模型。对于理想飞行纵向模型,分别计算了飞机在着陆前特定飞行空间内三种襟翼设置模式下连续系统的后向可达集,作为飞行员在着陆前选择飞行模式的依据。对于简化的6自由度人在环模型,计算了飞机在降落初期给定时间段内的后向可达集,为飞行员提供安全飞行状态空间。此外,本文考虑了实际飞行过程中飞行员操作引起的离散模式切换,计算飞机在混杂过程中的可达集,并以此作为飞行状态的安全性判据。对于理想的纵向模型,飞行员合理及时的操作能够保证飞机在模式切换过程中飞行于最大可控的安全飞行包线;对于6自由度人在环模型,计算所得的后向可达集能够提示飞行安全状态范围,以便飞行员及时做出调整。在考虑人为因素的情况下,当飞行员判断失误或操作延迟发生时,可达集仍可作为有效的安全性判据,反映飞行安全状态的趋势。