8.4 安全性、活性及公平性

8.4安全性、活性及公平性第8章模型检测2026年4月计算机科学中的数理逻辑目录CONTENTS01安全性vs.活性学习系统性质的两个基本分类：安全性和活性，理解它们的核心思想和区别。02公平性假设了解为什么需要公平性假设，以及常见的公平性类型。01安全性vs.活性SAFETYVS.LIVENESS形式化验证·基础性质安全性(Safety)核心思想“坏事永远不会发生”(Nothingbadeverhappens)关注系统在运行过程中，绝对不能进入的“坏”状态或执行路径。本质特征若一个执行违反了安全性，我们总能找到一条有限的前缀路径来证明这一违反行为，且该路径之后的任何延伸都无法改变这个事实。1.形式化定义任何违反该性质的执行，都必然存在一个有限的前缀，使得所有延伸该前缀的执行都违反该性质。2.通俗理解：“禁令”系统必须遵守的负面约束，即绝对不允许发生的情况：

•程序在运行中不会崩溃

•银行账户的余额永远不会为负3.经典示例：互斥性•要求：在任意时刻，系统中最多只有一个进程能位于临界区。

•“坏事”：有两个或两个以上的进程同时进入了临界区。活性(Liveness)💡核心思想“好事终将发生”(Somethinggoodeventuallyhappens)。它是与“坏事永不发生”的安全性(Safety)并列的、衡量系统正确性的两大支柱之一。📝通俗理解活性是系统需要保证的“正向承诺”，关注系统的进展性：•程序最终会终止并给出结果

•网络数据包最终会被送达

•对共享资源的请求最终会被响应01/形式化定义任何有限的执行片段，都可以被延伸为一个满足该性质的无限执行。

简单说：无论当下如何，未来总有机会达成目标。02/关键特征•关注进展：确保系统不会陷入永久的“停滞”状态。

•无限路径：违反活性性质的执行通常是无限长的——因为“好事”永远没有发生。03/示例：无死锁与无饿死•无死锁：进程不会因互相等待而永久阻塞。

•无饿死：进程对临界区的申请最终一定能被满足。这里的“好事”，就是进程成功进入临界区。安全性与活性的关系01/安全性(Safety)关注点：避免“坏”事发生，确保系统不会进入不可接受的状态。违反路径：有限的。一旦发生违规行为，在有限的步骤内就能被检测到。本质：系统的“禁令”。它定义了系统必须遵守的底线和不可逾越的规则。02/活性(Liveness)关注点：确保“好”事最终发生|违反路径：无限的|本质：系统的“承诺”活性关注系统的进展和最终目标达成，例如“最终会处理请求”或“最终会释放锁”。它的违规行为无法在有限时间内被检测。💡核心总结任何非平凡的系统性质，都可以逻辑地表示为“一个安全性性质”和“一个活性性质”的合取。二者互补，共同构成了对系统行为完整且严谨的逻辑描述。示例：互斥访问问题系统模型基于信号量的两进程互斥访问迁移系统。该模型展示了两个进程在临界区与非临界区之间的状态流转关系。性质分析：安全性与活性分析互斥访问系统的两个关键性质，确保安全性与活性。🔒安全性(Safety):互斥性系统绝不应该进入“坏”状态。在本模型中，需严格检查是否存在任何状态，导致两个进程同时处于临界区（如c1和c2同时为真）。♾️活性(Liveness):无饿死(StarvationFreedom)系统最终会进入“好”状态。需验证：从任何一个进程请求进入临界区的状态出发，该进程总能最终到达临界区，不会永远等待。总结：互斥性保证了系统运行不出错，而无饿死性质则保证了系统运行有“进展”，二者缺一不可。02公平性假设FAIRNESSASSUMPTIONS为什么需要公平性假设？核心思想：排除那些“无限拖延”或“无限优先”的不切实际的执行路径，聚焦系统在合理逻辑下的真实行为模式。定义：公平性假设是对系统执行路径的一种约束条件。在形式化验证中，模型检测器只会将满足该假设的执行路径纳入验证范围，忽略那些违反公平性的逻辑路径。必要性与理论挑战许多关键的活性性质（如“无饿死”或“最终响应”）在缺乏公平性假设时无法被严格证明，因为逻辑上始终存在一条“无限偏袒部分进程”的不公平路径作为反例，导致验证失败。工程实践中的价值现实的软硬件系统（如操作系统调度器、通信协议）都隐含公平性特征。例如，一个设计良好的调度器不可能无限期忽略一个已就绪的进程。引入该假设，能确保验证结论与系统的实际运行行为一致。常见的公平性假设类型01/弱公平性(WeakFairness)定义：如果一个进程无限次地被启用，那么它最终必须被执行。弱公平性也常被称作“进展性”。示例：在操作系统的进程调度中，调度器不能无限期地忽略一个处于就绪状态的进程，无论其优先级如何，它最终都必须获得CPU执行权。02/强公平性(StrongFairness)定义：如果