【形式化验证基础】活跃属性Liveness Property和安全性质（Safety Property）介绍

一、Liveness Property

1、概念介绍

在系统的形式化验证领域，活性属性（Liveness Property）是一个至关重要的概念。与安全性质（Safety Property）侧重于防止系统出现不良行为不同，活性属性主要关注系统能否最终达成某些期望的目标或事件。

从定义上来说，活性属性描述了系统在运行过程中，某些积极的、有益的事件最终必然会发生的特性。例如，在一个任务调度系统中，活性属性可以是每个任务最终都能得到执行；在一个通信系统里，活性属性可能意味着发送的消息最终会被接收。

活性属性的核心在于“最终会发生”这一概念。它并不关心事件何时发生，也不关心在事件发生之前系统经历了哪些中间状态，只强调事件一定会在未来的某个时刻出现。这种特性使得活性属性在描述系统的长期行为和目标达成方面具有独特的价值。

以一个简单的电梯控制系统为例，活性属性可以表述为：“每一个楼层的电梯请求最终都会被响应”。在这个系统中，无论电梯当前处于何种状态，是正在运行、停靠还是空闲，只要有新的楼层请求发出，按照活性属性的要求，这个请求最终一定会得到处理，电梯会到达相应楼层。

再看一个网络传输的场景，假设发送方不断地向接收方发送数据，活性属性可以是“发送的数据最终都会被接收方成功接收”。这意味着即使在传输过程中可能会遇到网络延迟、丢包等问题，但从长远来看，所有发出的数据都能顺利抵达接收端。

2、形式化定义

在不同的形式化验证领域，描述活性属性（liveness Property）的数学公式会因使用的逻辑系统而有所不同，以下主要介绍基于线性时序逻辑（LTL）和计算树逻辑（CTL）的常见公式。
1）. 基于线性时序逻辑（LTL）的公式
- 最终发生公式：在LTL中，“最终（finally）”操作符$\mathbf{F}$用于表达某个事件最终会发生。例如，若有一个命题$p$表示“任务完成”， 公式$\mathbf{F}p$就表示“任务最终会完成”。更复杂一点，若系统中有“资源请求（request）”和“资源分配（grant）”两个事件，公式$\mathbf{F}(request\to \mathbf{F}grant)$表示一旦发出资源请求，最终会得到资源分配 。
- 直到公式：“直到（until）”操作符$\mathbf{U}$可用于描述活性属性。对于命题$p$和$q$，公式$p\mathbf{U}q$表示$p$一直为真，直到$q$成立。例如，在一个循环执行的任务系统中，设$p$为“任务处于执行中”，$q$为“任务成功完成”，$p\mathbf{U}q$意味着任务会一直执行，直到成功完成。
- 释放公式：“释放（release）”操作符$\mathbf{R}$与$\mathbf{U}$对偶。公式$p\mathbf{R}q$表示$q$一直为真，直到$p$为真且$p$持续为真（包括$p$首次变为真的时刻）。比如在一个数据传输系统中，$p$表示“数据传输通道正常”，$q$表示“数据在缓存中等待传输”，$p\mathbf{R}q$表示数据会在缓存中等待，直到传输通道正常且保持正常状态 ，数据才开始传输。
2）. 基于计算树逻辑（CTL）的公式
- 所有路径上最终发生公式：在CTL中，路径量词$\mathbf{A}$表示“所有路径”，结合“最终”操作符$\mathbf{F}$，公式$\mathbf{AF}p$表示在所有可能的执行路径上，命题$p$最终都会成立。例如，在一个多线程并发系统中，$p$表示“所有线程执行完毕”，$\mathbf{AF}p$表示无论线程如何并发执行，所有线程最终都能执行完毕。
- 存在路径上最终发生公式：路径量词$\mathbf{E}$表示“存在路径”，公式$\mathbf{EF}p$表示存在一条执行路径，使得命题$p$最终成立。比如在一个故障容错系统中，$p$表示“系统从故障中恢复正常运行”，$\mathbf{EF}p$意味着存在一种可能的故障处理路径，能让系统最终恢复正常 。

二、Safety Property

1. 定义回顾

一个轨迹集合Φ被称为安全性质（Safety Property），如果对于每一个不在Φ中的轨迹σ，存在某个有限的前缀σˆ，使得没有任何Φ中的轨迹以这个σˆ作为开头。换句话说，每一个不满足安全性质的轨迹都有一个“坏前缀”，一旦发生这个坏前缀，就可以确定该轨迹违反了安全性质。

2. 核心概念解析

• 轨迹（Traces）：系统的运行轨迹，描述系统状态随时间的变化序列。系统在运行过程中，从初始状态开始，随着时间推移，不断地改变自身状态，这些状态的变化顺序就构成了轨迹。例如，在一个简单的计数器系统中，轨迹可能是[初始值为0，加1后变为1，再加1后变为2，……]这样的状态序列。
• 安全性质Φ：所有满足特定安全约束的轨迹集合。例如，在交通信号灯系统中，Φ可能是所有“任何时候只有一个颜色亮着”的轨迹。这就定义了交通信号灯系统在安全运行状态下的所有可能的状态变化序列，只有符合这一约束的轨迹才属于安全性质的范畴。
• 坏前缀σˆ：一个有限的轨迹开头部分，一旦发生这个部分，就可以确定整个轨迹违反了安全性质。这意味着没有任何满足安全性质的轨迹会以这个σˆ作为开始。比如在交通信号灯的例子中，如果出现了“绿灯和红灯同时亮起”的状态作为轨迹的开头部分，那么这个轨迹就违反了“任何时候只有一个颜色亮着”的安全性质，“绿灯和红灯同时亮起”就是一个坏前缀。

3. 为什么强调“有限前缀”

安全性质的一个关键特性是其可验证性。如果任何违反都会在有限的时间内被检测到，那么我们就可以通过监测系统状态的变化，在违反发生时立即采取措施，而不是无限期地等待可能永远不会发生的违反。从实际操作的角度来看，有限前缀使得安全性质的验证变得可行。在复杂的系统中，我们不可能一直观察系统的无限运行过程来判断其是否安全。通过关注有限前缀，一旦发现坏前缀，就能及时发出警报、停止系统运行或者进行纠错操作，从而避免可能出现的严重后果。而且，这也使得自动验证工具能够有效地检查系统的安全性，大大提高了验证的效率和可靠性。

4. 示例说明

4.1 示例1：交通信号灯系统

• 安全性质Φ：所有满足“任何时候只有一个颜色亮着”的轨迹。这是交通信号灯系统正常运行的基本安全约束，确保交通秩序和交通安全。
• Traces(S) \ Φ：所有在某些时刻有多个颜色同时亮起的轨迹。这些轨迹违反了安全性质，属于不安全的运行情况。
  根据定义，对于每一个违反Φ的轨迹σ（例如，在某个时间点绿灯和红灯同时亮起），存在一个有限前缀σˆ。这个σˆ可能是“绿灯和红灯同时亮起”的状态。一旦发生这样的情况，就可以确定该轨迹违反了安全性质，因为没有任何满足Φ的轨迹会以这个σˆ作为开头。在实际的交通信号灯控制中，一旦检测到这种坏前缀情况，就可以立即启动故障处理机制，比如切换到闪烁黄灯模式，提醒驾驶员注意安全，同时通知维护人员进行维修。

4.2 示例2：银行账户管理系统

• 安全性质Φ：所有满足“任何时候账户余额不能为负”的轨迹。这是保障银行账户资金安全和正常交易的重要约束。
• Traces(S) \ Φ：所有在某些时刻账户余额变为负数的轨迹。这些轨迹表示账户出现了异常情况，可能导致经济风险。
  根据定义，对于每一个违反Φ的轨迹σ（例如，在某次交易后账户余额变为负数），存在一个有限前缀σˆ。这个σˆ可能是“账户余额变为负数”的状态。一旦发生这样的情况，就可以确定该轨迹违反了安全性质，因为没有任何满足Φ的轨迹会以这个σˆ作为开头。银行系统在检测到账户余额变为负数的坏前缀时，会立即冻结账户交易，防止进一步的资金损失，并通知账户持有人解决欠款问题。

5. 实际应用的意义

• 及时检测与响应：通过识别坏前缀，系统可以在违反安全性质的第一时间被检测到，从而允许采取纠正措施或停止危险操作。在工业控制系统中，安全性质可以定义为某些关键设备的温度、压力等参数不能超过安全阈值。一旦检测到参数超过阈值的坏前缀，系统可以立即启动降温、降压等措施，或者直接停止设备运行，避免发生爆炸、泄漏等严重事故。
• 可验证性：有限时间内的检测使得自动验证工具能够有效检查系统的安全性，而无需考虑无限的时间范围。这大大提高了系统开发和维护的效率。在软件开发过程中，利用形式化验证工具对程序进行安全性质的验证，可以在早期发现潜在的安全漏洞，减少后期修复漏洞的成本和风险。

三. 总结

在实际应用中，活性属性的意义不可小觑。它为系统的正确性提供了一种动态的保障。如果一个系统仅仅满足安全性质，只能保证不出现错误状态，但可能会陷入停滞，无法实现其预期功能。而活性属性则确保了系统能够持续推进，完成其应有的任务。例如在工业自动化生产线上，活性属性保证了各个生产任务能够依次执行，产品得以顺利生产出来，而不是因为某些条件一直不满足而导致生产线停滞。同时，在分布式系统中，活性属性对于保证系统的可用性和可靠性至关重要，确保各个节点之间的交互和任务最终都能完成，避免出现死锁或无限等待的情况。

然而，验证活性属性也面临一些挑战。由于活性属性关注的是系统的最终行为，可能需要考虑系统的长期运行情况，这对于验证工具和方法来说是一个考验。不像安全性质可以通过检测有限前缀来判断是否违反，活性属性往往需要对系统的整个运行轨迹进行分析，甚至要考虑无限的时间范围，这增加了验证的复杂性。