本文是软件工程论文，为了在实践中开发高质量的安全关键系统，开发一种对需求工程师友好、严格且高效的方法是很重要的。然而，在这三个指标之间达成平衡几乎总是需要权衡的。在这项工作中，本文展示了如何使用轻量级形式化方法来验证和定位实时安全需求中的不一致性，从而达到平衡.主要工作包括以下几点：为了描述实时安全需求,本文对安全模式语言（SafeNL）进行基于实时约束的扩展,得到实时安全模式语言。RTNL将需求中的实时约束和因果关系描述为事件和事件之间的关系，给出相应的语法定义，并通过一个示例来对RTNL进行应用。本文对实时安全需求的不一致性进行验证和定位，包括行为不一致性验证和定位、循环不一致性验证和定位以及实时不一致性验证和定位。最后，基于实时安全模式语言对需求的行为不一致性进行验证，基于因果时钟图对需求的循环不一致性验证，并基于实时时钟图对需求的实时不一致性进行验证。接下来，将需求从实时安全模式语言自动转换为时钟图，然后根据验证所需要的实时关系和因果关系，将时钟图分别转换为实时时钟图和因果时钟图。
........
第一章绪论
为了跨越自然语言与形式化的鸿沟以及解决现有的基于形式化方法的解决方案效率低的问题，本文提出基于模式语言的形式化表示和基于图形的高效算法来验证实时安全需求中的不一致性，包括行为不一致性、循环不一致性以及实时不一致性。具体来说，我们对安全模式语言进行扩展得到新的实时安全模式语言，增加了实时约束使其能描述实时安全需求。使用时钟约束规范语言（CCSL）为实时安全模式语言提供形式化语义，然后将CCSL转换为图。我们将需求的行为不一致性验证转换为冲突模式的匹配问题，将循环不一致性验证转换为图的搜索问题，以及将实时不一致性验证转换为图的计算问题。与基于模型检测的一致性验证方法相比，这是轻量级的验证方法，可以满足大规模需求。图1.1对本文的研究思路进行描述，主要包括以下三个阶段：实时安全需求的表示，形式化表示的转换，以及需求的不一致性验证。首先，使用实时安全模式语言对实时安全需求进行描述。
.....
第二章预备知识
2.1CCSL
本文的主要工作包括：本文将行为不一致性验证问题转换为冲突模式的匹配问题。基于需求中的常见问题，本文预定义了一组常见的冲突模式，并提供了一个算法，根据冲突模式直接过滤出存在行为不一致性的需求。基于因果时钟图，本文将循环不一致性的验证问题转换为图的搜索问题，然后基于因果时钟图中检测到的循环依赖关系，对需求中的循环不一致性进行定位，并提供了算法对因果时钟图中的循环依赖进行扩展，以此来对需求循环不一致性产生的情况进行说明，辅助需求工程师对需求进行修改。若允许通话列车在该进路线上运行，则通话列车前方不得有非通话列车在该路线的第一子路上运行（0009）。这与需求0006种的非通话列车运行在第一子路上运行相冲突。这些CCSL约束被转换成具有80个节点和117个边的CCG。案例2的文件包含11个安全需求，这些需求被转化为28条RTNL语句和121条CCSL约束。最后，得到包含67个节点和131条边的CCG。利用这些RTNL语句和CCG，可以得到以下结果。对于案例1（一致性文档），在行为不一致性验证中没有发现冲突，在循环不一致性验证中也没有发现循环依赖。对于案例2（不一致文档），首先在进行行为不一致性验证时，根据冲突模式3，算法5.1确定RTNL语句0005和0008是冲突对，表示为<0005，0008>。
2.2SafeNL
安全模式语言（SafeNL）[10]用于对安全需求进行描述。它具有以下特点：1）SafeNL是一种类自然语言，很容易将需求规范从自然语言转换为SafeNL文档，便于需求工程师对安全需求进行描述；2）SafeNL拥有形式化语义，可以被自动的转换为CCSL，实现对需求的形式化描述。SafeNL中捕捉到了与安全需求相关的三种常见现象，即事件、状态以及他们之间的关系，其中状态也可以用两个事件及其之间的关系来描述。为了描述实时安全需求，本文选择对[10]中的安全模式语言（SafeNL）进行扩展，加入时间约束得到新的实时安全模式语言（RTNL），来对实时需求进行描述。我们发现实时需求有三个基本要素：事件、状态和时间约束。事件和状态都是被约束的对象，但我们假设事件不花费时间，而状态花费时间。实际上，每个状态都可以表示为开始事件、结束事件及其持续时间。因此，基于事件和事件之间的关系，本文通过CCSL提供了RTNL语言的语义。根据约束对象数量的不同可以将RTNL分为简单模式和复合模式，其中简单模式指的是一个子句只对某一个状态或事件进行约束，而复合模式则是指一个子句中对多个状态和事件进行约束。我们分别对其进行描述。
第三章RTNL模式语言设计....................15
3.1简单模式..................................15
3.2复合模式..................................24
3.3RTNL模式语言的应用..........................25
第四章RTNL到实时时钟图和因果时钟图的转换....................29
4.1图的定义..................................29
4.2RTNL到CCSL的转换..........................32
4.3构造实时时钟图和因果时钟图......................37
第五章实时安全需求不一致性验证和定位方法....................41
5.1运行案例..................................42
5.2基于冲突模式的行为不一致性验证...................44
5.3基于循环依赖的循环不一致性验证...................46
5.4基于实时时钟图的实时不一致性验证..................50
......
第六章案例研究与评估
6.1工具实现
本章将给出本文方法的支撑工具，并以两个轨道交通中的实际应用案例以及一个自动驾驶领域的实际案例对本文方法的有效性进行证明。通过设计不同的对比实验，对本文提出的行为一致性验证方法、循环一致性验证方法以及实时一致性验证方法进行分析和评估。为了支撑以上工作，本文实现了其支撑工具——需求一致性验证器ConsistencySR。该工具使用Java1.8实现其后端功能，使用Angular8作为其前端框架，其系统架构图如图6.1所示，包括表现层、业务逻辑层和数据持久层。其中表现层为需求工程师与工具交互的接口，业务逻辑层实现RTNL到CCSL的自动转换、CCG和RCG的自动构造、行为不一致性的验证和定位、循环不一致性的验证和定位、基于SMT的逻辑一致性验证以及实时一致性的验证和定位，数据持久层存储RTNL输入、中间模型和最终验证结果。然后允许第一列非通话列车在该线路上运行（0008）。当非通话列车已在该进路的第一条子路上运行，且检测到第一条子进路被占用时，未分配进路的信号机在5s后应变为受限（0006）。在5s延迟时间内，可以完成以下操作。即当进路信号允许且进路尚未分配时，该进路应分配给信号机前同方向的第一辆通话列车（可与控制中心通信的列车）（0001）。当被分配的通话列车头越过进路信号机（0002）时，进路信号机应变为受限。如果一条进路被分配给一辆通话列车，则允许列车在该进路上运行（0007）。
6.2案例研究
为了验证本文方法的有效性，使用卡斯柯信号有限公司的两个安全需求文档以及汽车照明系统的需求文档，分别分析行为不一致性验证、循环不一致性验证以及实时不一致性验证的有效性。由于行为不一致性和循环不一致性都是不涉及需求中的实时约束，因此将这两种放在一起讨论他们的有效性。将卡斯柯信号有限公司的两个由自然语言编写的安全需求文档转换为RTNL文档，然后转换为CCSL约束。案例1的文档包含17个安全需求，从中导出了20条RTNL语句和120条CCSL约束。表6.1给出了自然语言和RTNL描述的需求。当得到存在行为不一致性冲突对<0005，0008>时，需求工程师需要决定哪一句话是有问题的。假设他们决定删除需求0005，文档的其余部分可以继续进行循环不一致性验证。算法5.2检测到CCG中存在两组循环依赖（如图6.3所示）。然后，根据RTNL和CCSL的对应关系，就可以得到可能导致循环不一致性的RTNL语句。在案例2中，RTNL文档反映了以上冲突，使得0011，0008，0006，0001，0002，0007和0009由于循环依赖而被标记为循环不一致。我们对不一致性产生的原因进行解释：一开始，线路没有分配，这条线路上也没有列车。当一列（第一列）非通话列车（不能与控制中心通信的列车）到达时，进路信号机应变为允许（0011）。
....
第七章总结与展望
其中行为不一致性验证方法定义了一组常见的冲突模式，并提供了一个算法，根据冲突模式直接过滤出存在行为不一致性的RTNL语句；循环不一致性的验证通过CCG的循环依赖搜索实现，然后基于CCG中检测到的循环依赖关系，对需求中的存在循环不一致性的最小集合进行定位，并提供了算法对CCG中的循环依赖进行扩展，以此来对需求循环不一致性产生的情况进行说明，辅助需求工程师对需求进行修改；实时不一致性的验证方法定义了RCG中节点的发生条件，将实时不一致性的验证问题转换为图的计算问题，提供了实时不一致性的自动验证算法，并根据检测结果对RTNL中的最小不一致集进行定位。最后，实现了需求一致性验证器ConsistencySR作为本文方法的支撑工具，并通过工业界中的案例对该方法的有效性进行验证。同时，为了说明该方法的优势，本文设计了多组对比实验进行评估。实验结果证明，该方法具有高效性，并且可以在复杂的大规模安全攸关系统中应用。
参考文献（略）
