安全关键系统广泛应用于各种行业领域,例如国家的航空航天项目以及近年来迅速发展的无人驾驶、智慧医疗等领域。该类系统对安全性有着极高要求,一旦出现系统失效即可能造成重大的生命财产损失,因此,如何保障该类系统的安全性一直是学术界以及工业界的重要议题。安全性需求描述了系统不应发生的危险状态,来源于系统的早期危害分析以及后续的安全性分析迭代,尽早对其验证可以有效提高系统安全性。然而,在实际的系统开发过程中,系统设计模型基于功能需求进行开发,这导致了安全性需求与系统设计之间存在沟壑,使得设计模型是否满足安全性需求难以验证,系统的安全性难以得到有效的保障。针对以上问题,本文提出了一种基于SysML面向安全关键系统的安全性需求追踪及验证方法。本文主要研究内容如下:首先,参照相关安全标准,提出一个面向安全关键系统的追踪信息模型用于指导建模中追踪信息的捕获;接着,针对标准SysML需求图缺乏描述安全性需求能力,本文对SysML需求图进行了扩展,使其可以建模安全性需求并捕获追踪信息;此外,针对SysML需求图缺乏安全性需求追踪信息的导出机制,文中通过模型转换将需求图转换到追踪信息表达模型,生成独立的追踪信息文档,为后续安全性验证提供直接支持。其次,利用追踪信息定位SysML设计模型中用于实现安全性需求的SysML块以及块中元素,根据定位到的安全关键SysML设计给出算法构建面向验证的SysML块定义图进行安全性验证;但由于SysML模型缺乏精确语义,难以直接进行验证,故而本文中接着给出了从SysML模型转换到NuSMV形式化模型的规则,将SysML块定义图和状态机图转换到可验证的NuSMV系统模型,通过模型检测器验证安全性需求满足情况。最后,使用本文的方法对一个铁路控制系统进行案例分析。通过验证发现了系统设计中存在的缺陷,有效识别了潜在风险,同时也说明了本文方法的有效性。本文方法提供了一种安全关键系统中可追踪性建立以及利用追踪信息在系统开发早期定位系统安全关键组件并验证安全性的可行思路。