如何对安全关键混成系统进行形式化建模及验证方法是一项重要的科学问题。在现有的工程实践中,作为验证对象的安全属性缺乏规范化的获取方式;工业应用广泛的形式化建模语言LUSTRE不支持对物理世界连续行为的建模;系统的高复杂度带来的状态空间爆炸问题使得验证无法完成。这些难点的存在阻碍着安全关键混成系统的安全性的进一步提高,已经成为了安全关键软件行业不可回避的挑战。本文以构建安全关键混成系统建模与验证方法为研究目标,从分析需求规约出发,针对形式化验证方法中模型检验方法的特征,提出了一套可行的规范化流程,主要贡献包括:·提出了安全关键混成系统建模及验证框架。该框架从需求规约出发,覆盖了对系统进行需求建模、需求分解、设计建模、验证实现等步骤,解决了从需求出发难以构建对系统进行验证所需的组件的问题。·提出了两种基于投影的问题分解方法。这两种方法都以问题框架方法为基础,分别从子需求和变量约束的角度寻找投影维度,对问题模型进行分解。从而降低了描述安全关键混成系统的问题的复杂度。·定义了混成系统建模语言Hybrid LUSTRE。该语言以同步建模语言LUS-TRE为基础,结合混成自动机时间模型,给出了形式化的语法和语义,使其能够描述物理世界的连续行为,从而支持对混成系统进行建模,解决了安全关键混成系统的连续行为描述的问题。·提出了对安全关键混成系统的验证方法。该方法以框架中的建模方法为基础,针对形式化验证的特征进行了相应优化。并具体定义了验证问题中各个模块在不同建模阶段的设计与实现方法。本文所提出的方法已经成功应用于轨道交通列车控制系统的工业应用之中。结果显示,本框架的使用有效地简化了安全关键混成系统的建模与验证流程。其中,系统的验证耗时降低了约20%,提高了可以被验证的系统的规模,在一定程度上缓解了状态空间爆炸问题。该应用首次完成了项目级的区域控制器安全关键模块的形式化验证。