Safety Property

释义 Definition

安全性性质（常用于形式化验证、模型检测与并发系统）：指一种系统性质，强调“坏事永远不会发生”。也就是说，系统在任何运行过程中都不应到达某些被禁止的状态（例如越界访问、死锁、违反互斥等）。
（相关概念：与之相对的常见类别是 liveness property “活性性质”，强调“好事最终会发生”。）

发音 Pronunciation (IPA)

/ˈseɪfti ˈprɑːpərti/（美式常见）
/ˈseɪfti ˈprɒpəti/（英式常见）

例句 Examples

A safety property says the program never reads past the end of an array.
安全性性质表示程序永远不会读到数组末尾之外。

In model checking, we often prove a safety property by showing that no reachable state violates the invariant under all possible interleavings.
在模型检测中，我们常通过证明在所有可能的交错执行下，没有任何可达状态会违反不变式，从而证明一个安全性性质。

词源 Etymology

safety 来自 safe（安全的），表示“免于危险”；property 在逻辑与计算机科学语境中常指“性质/属性/命题”。组合成 safety property，在形式化方法中被固定用来指代“禁止不良行为发生”的一类系统性质。

相关词 Related Words

• Invariant
• Liveness
• Deadlock
• Mutual Exclusion
• Model Checking
• Temporal Logic
• Reachability
• Assertion

文学与经典著作 Literary Works

• Principles of Model Checking（Christel Baier, Joost-Pieter Katoen）——系统讲解安全性/活性性质与验证方法。
• Model Checking（Edmund M. Clarke, Orna Grumberg, Doron A. Peled）——将 safety property 作为核心性质类型讨论。
• Communication and Concurrency（Robin Milner）——在并发系统语境下讨论可验证的安全相关性质。
• Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers（Leslie Lamport）——用规格说明与不变式等方式表达并验证安全性性质。