基于UPPAAL的双线程建模优化：移除线程间通道同步依赖

原始伪代码 #

sleep_time = 10;
deadline_time = 2;

主线程：

while(true){
write(); // 已定义的函数
sleep(sleep_time);
}

线程2：

while(true){
if(write函数每2秒（deadline_time）被调用一次){
} 
else {
callback_function();
}
}

问题修正方向 #

原建模通过通道同步人为建立了线程间依赖，不符合实际代码中线程独立的逻辑，需改用全局时间戳+时钟驱动的方式实现无依赖建模。

详细修改方案 #

1. 声明部分（中文翻译） #

• 全局共享变量：上次写入时间戳（记录主线程最近一次调用write()的时间）
• 全局常量：休眠时长 = 10，超时阈值 = 2
• 状态变量：
  • 主线程状态：执行写入/休眠中
  • 线程2状态：检查超时

2. 主线程自动机调整 #

移除所有通道相关动作，核心修改为执行write()时更新全局时间戳：

• 初始状态 → 触发write()（同步更新上次写入时间戳为当前系统时间） → 进入休眠中状态（持续休眠时长） → 回到初始状态循环

3. 线程2自动机调整 #

移除所有通道相关动作，改为基于时间戳的周期性检查：

• 初始状态 → 计算当前系统时间 - 上次写入时间戳：
  • 若差值 > 超时阈值：触发callback_function() → 回到初始状态循环
  • 若差值 ≤ 超时阈值：直接回到初始状态循环

验证逻辑 #

当休眠时长 > 超时阈值（即10>2）时，主线程两次write()的间隔超过2秒，线程2会检测到超时并触发回调，进入unsafe_state；当休眠时长 ≤ 超时阈值时，两次写入间隔符合要求，不会触发回调，完全匹配需求场景。

内容的提问来源于stack exchange，提问作者Meta Overflow