Page 61 - 《软件学报》2025年第12期

5442 软件学报 2025 年第 36 卷第 12 期

σ 的长度大于 0 P 的语义如图 1(c) 所示; A4 公
区间 σ 上成立, 当且仅当 并且在子区间 σ (i...|σ|) (0 ⩽ i ≺ |σ|) 上成立,
−
式是基本操作符; A5 公式的投影操作符 prj 是 PPTL 的核心操作符, 它可以描述进程间并发和同步操作. 如图 2 是
投影公式 (P 1 ,P 2 ) prj Q 的语义表示. P 1 和 Q 在状态 t 0 同时开始执行. 在整个过程中, Q 和 P 1 ;P 2 在一段时间内并行
执行, 但可能存在 3 个不同的时间点结束, 3 种可能的结果分别为: (1) Q 在 P 2 之后结束, (2) P 2 和 Q 同时结束,
(3) Q 在 P 2 之前结束.

◊P P P

··· ··· ··· ··· ··· ··· ···
S i S |σ| S i S |σ|
S 0 S i S |σ|
S 0 P S 0
P
P
P
(a) (b) (c)
♢P、 P 的语义
图 1 公式 □P 和

t 0 t 2 t 4 t 5 t 0 t 2 t 4 t 0 t 2
Q Q Q
t 0 t 1 t 2 t 3 t 4 t 0 t 1 t 2 t 3 t 4 t 0 t 1 t 2 t 3 t 4
P 1 P 2 P 1 P 2 P 1 P 2
(P 1 ,P 2 ) prj Q 的语义
图 2 公式

2.4 监控语义
监控语义是在运行时验证 (runtime verification, RV) 中, 系统通过实时监控其行为并根据预定协议及时反馈,
以检测错误或违规情况. 通常, 运行时验证利用形式化规范语言来定义安全性质 φ, 当使用 PPTL 来描述监控语义
时, 首先定义系统的期望性质, 并将相应的 PPTL 公式转换为监控器, 即一个有限状态自动机 (finite state machine,
FSM). 传统 PPTL 使用二值语义来进行判定, 输出结果为 true 或 false. 然而, 由于系统在执行过程中会产生无限状
态的轨迹, 并且在没有外界干扰的情况下是非终止的, 运行时验证无法获取系统的完整执行轨迹, 因此无法用二值
语义来全面描述其性质. 为了应对这一问题, 引入一个额外的真值 inconclusive 扩展 PPTL 的值域, 其定义 [21] 如下:

∑
 ω
 true, ∀ω ∈ : uω|= φ







 ∑

[u |= φ] =  false, ∀ω ∈ ω : uω|, φ (4)








inconclusive, otherwise

∑
其中, 表示字母表. 对于一个性质 φ 和一个有限前缀 u, 如果 u 的所有扩展都满足该性质, 则说明 u 满足 φ; 如果
u 的所有扩展都违反了性质, 则说明 u 违反了 φ; 否则, 它无法说明 u 是否满足或违反了性质 φ.
语法语义的定义为数据预处理及结果准确性评估做了理论铺垫, 数据预处理中筛选的重点携带时序逻辑语义
的单词来源于定义中时序逻辑符号. 依存关系提取的时序逻辑依赖关系, 也来源于定义中的时序逻辑关系, 数据预
处理实现了有效的特征信息提取, 从而保障了神经网络分类准确的性能. 此外, PPTL 的语义识别的正确性评估遵
循严格的数理逻辑定义, 其通过高阶张量运算构建的时序标签向量与时序符号定义应具有语义一致性, 确保网络
能够计算精确的关系得分, 得到需求文本的真实时序逻辑语义分析结果.
3 基于小样本网络的时序逻辑语义分析 FSLNets-TLSA
鉴于深度神经网络强大的表示能力和特征提取能力, 本文提出一种基于小样本网络的时序逻辑语义分析方
法, 该方法的整体架构如图 3 所示.