文章目录
- 一、Liveness Property
-
- 1、概念介绍
- 2、形式化定义
- 二、Safety Property
-
- 1. 定义回顾
- 2. 核心概念解析
- 3. 为什么强调“有限前缀”
- 4. 示例说明
-
- 4.1 示例1：交通信号灯系统
- 4.2 示例2：银行账户管理系统
- 5. 实际应用的意义
- 三. 总结
一、Liveness Property
1、概念介绍
在系统的形式化验证领域，活性属性（Liveness Property）是一个至关重要的概念。与安全性质（Safety Property）侧重于防止系统出现不良行为不同，活性属性主要关注系统能否最终达成某些期望的目标或事件。
从定义上来说，活性属性描述了系统在运行过程中，某些积极的、有益的事件最终必然会发生的特性。例如，在一个任务调度系统中，活性属性可以是每个任务最终都能得到执行；在一个通信系统里，活性属性可能意味着发送的消息最终会被接收。
活性属性的核心在于“最终会发生”这一概念。它并不关心事件何时发生，也不关心在事件发生之前系统经历了哪些中间状态，只强调事件一定会在未来的某个时刻出现。这种特性使得活性属性在描述系统的长期行为和目标达成方面具有独特的价值。
以一个简单的电梯控制系统为例，活性属性可以表述为：“每一个楼层的电梯请求最终都会被响应”。在这个系统中，无论电梯当前处于何种状态，是正在运行、停靠还是空闲，只要有新的楼
