安全需求的质量直接关系到系统的成败,乃至人们的生命财产安全。随着系统规模的增大,安全需求急需自动化的精确分析。很多安全标准推荐使用形式化方法,但现在大部分公司仍然使用自然语言对需求进行描述。为了跨越自然语言与形式化的鸿沟以及解决现有的基于形式化方法的解决方案效率低的问题,针对实时安全需求,本文定义了实时安全模式语言,赋予类自然语言表示的实时安全需求以形式化语义,并在此描述基础上定义了高效算法对实时安全需求的行为不一致性、循环不一致性以及实时不一致性进行验证。主要工作包括:■在安全模式语言的基础上,定义了实时安全模式语言。分简单模式和复合模式给出了语法,并用时钟约束规范语言CCSL提供了语义,这样就可以将类自然语言描述的需求直接对应到形式化的时钟约束规范语言中,为后续的分析验证奠定了基础。■定义了实时安全需求的行为不一致性和循环不一致性的验证和定位方法。行为不一致性验证方法预定义了一组常见的冲突模式,并提供了算法根据冲突模式直接过滤出存在行为不一致性的需求。循环不一致性验证方法将需求转换为因果时钟图,将循环一致性的验证问题转化为因果时钟图中循环依赖的搜索问题,然后基于检测到的循环依赖关系,对需求中的存在循环不一致性的最小集合进行定位,并设计了扩展算法来对循环不一致性产生的情况进行解释说明。■定义了实时安全需求的实时不一致性的验证与定位方法。将实时安全模式语言描述的实时需求转换为多个实时时钟图,将实时不一致性的验证问题转化为图的计算问题,提供了实时不一致性的自动验证算法,并根据验证结果对实时安全模式语言中的最小不一致集进行定位。最后,实现了需求一致性验证器作为本文方法的支撑工具,使用工业界中的案例验证了本文方法的有效性,并通过多组实验对本文方法的效率和适用规模进行评估。结果显示了本文方法的高效性,支持对大规模需求进行自动验证。