伴随实时系统在安全关键领域的广泛应用,其复杂度也在不断增加,如何保证实时系统安全性,避免财产损失甚至人员伤亡等灾难性事故的发生,已成为当前软件工程领域的研究重点。目前针对软件安全性分析的工作主要集中在软件需求规约阶段和功能设计阶段,其中以时间需求的描述及形式化规约为主要研究内容。然而在软件的实际开发过程中,对时间需求的分析及验证工作还很薄弱,时间需求一般以自然语言或结构化表述形式描述,难以直接转换到某种形式化体系。针对以上问题,本文利用模型检测技术,给出时间需求的规约方式,给出一种基于时钟约束规范语言(CCSL)的实时系统安全性验证方法。该方法通过时钟约束规范语言对原生时间需求的进一步描述,为之后时间需求的形式化表述提供便利。本文的主要研究内容如下:第一,为解决实时系统时间需求的分析验证问题,给出一种在软件需求分析阶段对时间需求进行形式化规约及验证的分析框架,借助时间自动机实现对时间需求的分析和验证工作。第二,借助EAST-ADL事件链模型及TADL时间约束,将模态顺序图中时间需求描述为带时间约束的事件链,之后给出事件链与CCSL规范的语义映射关系,设计了时间需求的分类表以及基于分类表和转换规则自动构建CCSL规范的算法。第三,通过时间自动机及其模型检测工具UPPAAL完成了对时间需求的形式化建模和验证。首先给出了CCSL和时间自动机元素之间的语义映射,并给出了几种常用时钟表达式的自动机表示形式,然后将时间约束失效状态的可达性作为待验证属性,最后在模型检测工具UPPAAL下对时间需求进行分析和验证。最后,运用本文给出的方法对电子刹车系统进行案例分析,给出建立系统事件链、CCSL规约及时间自动机模型的完整过程,通过对时间约束失效状态的验证和分析,发现了系统时间需求中的不满足性质,说明了本文方法的可行性和有效性,为实时系统时间需求分析工作提供了一种新的思路。