飞机作为一种工作在空中的交通工具,对安全性的要求极高,任何细微的差错都可能造成灾难性的后果,保障飞机的安全至关重要。现代飞机的各项功能都越来越依赖软件系统,然而现代机载软件功能繁多、结构复杂、构件众多,且影响因素多,设计阶段不能完全排除构件间相互影响尤其是软件安全性等级相互依赖而导致的整体安全下降的情况,为保证软件安全,开发人员需要在设计阶段就确保系统设计满足安全性要求。然而目前的方法不能完全满足安全性验证要求,因此亟需一种高效率地系统构件安全性验证方法以确保系统设计满足适航标准安全性要求。SysML语言被广泛用于系统工程建模,借助SysML语言可较好的描述机载软件架构及属性,但是SysML是半形式化的工具,缺乏精确语义的支持同时自身不具备验证的功能。Petri网是一种既有图形化特征也有精确语义的形式化工具,在形式化验证领域得到了广泛应用。通过适当的途径将SysML转化为Petri网模型,在此基础上可进一步验证软件的安全性,从而找出软件设计上的不足避免了后期返工及安全隐患,保证了系统的安全。本文分析了机载软件安全标准,在此基础上定义了一种适于描述机载软件安全一致性验证的扩展Petri网,其次基于SysML块图建立带安全属性的系统静态结构模型,构建SysML到Petri网的转换规则可将SysML块图转化为Petri网从而进行精确的形式化建模。然后,利用可达树图分析了系统安全状况的所有传递路径和所有的安全状态组合,在此基础上给出了安全性验证算法方法,验证软件构件安全等级设计是否符合适航标准。最后通过具体事例说明了方法的可行性,同时通过对比分析了基于Petri的安全验证方法的优势。