首页/论文/cs/0502046

arXiv cs/05020462005-02-09cs.LO

弱公平下活性性质的规范和细化的证明义务

Proof obligations for specification and refinement of liveness properties under weak fairness

Hector Ruiz Barradas, Didier Bert

摘要：

在这份报告中，我们提出了一个正式的模型，公平迭代的事件B事件系统。该模型用于证明基本活性属性的证明义务和一般活性属性的细化下的保存。事件的公平迭代模型使用燕尾算子，Broy和Nelson提出的一种算子来模拟公平选择。证明主要是建立在事件公平迭代和最弱前提演算的不动点计算上。

英文摘要：

In this report, we present a formal model of fair iteration of events for B event systems. The model is used to justify proof obligations for basic liveness properties and preservation under refinement of general liveness properties. The model of fair iteration of events uses the dovetail operator, an operator proposed by Broy and Nelson to model fair choice. The proofs are mainly founded in fixpoint calculations of fair iteration of events and weakest precondition calculus.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

分布式系统活性性质的精化

On the Refinement of Liveness Properties of Distributed Systems

我们提出了一种新的方法来推理分布式系统的活性特性，表示为自动机。我们的方法是基于模拟关系，只需要推理有限的执行片段。当前基于模拟关系的自动机活性属性推理方法需要对整个执行进行推理，因为它们涉及以下形式的证明义务：如果具体和抽象执行通过模拟“对应”，并且具体执行是活的，那么抽象执行也是活的。我们的贡献包括（1）定义活性性质的形式，（2）基于该形式的活性性质的证明方法，和（3）两个表达完备性结果：第一，我们的形式可以表示任何满足自然"鲁棒性“条件的活性性质，第二，我们的形式可以表示任何活性性质，只要历史变量可以使用

2008-01-07cs.LO

确保分布式系统的活性性质（研究议程）

Ensuring Liveness Properties of Distributed Systems (A Research Agenda)

为了建立分布式系统的活性属性，通常需要进行公平性假设，但在许多情况下，这些假设会导致错误的结论。本文件提出了一个研究议程，旨在奠定基础的并发性理论，配备，以确保分布式系统的活性属性，而不作出公平的假设。该理论将包括进程代数，时态逻辑和语义模型，以及实时处理。议程还包括开发一种方法，允许成功地应用这一理论的规范，分析和验证现实的分布式系统，包括无线网络的路由协议。当代进程代数和时态逻辑无法区分系统，其中一个具有关键的活性属性，另一个没有，至少在假设公正性时，强进展属性，但不假设公平性。建立一个替代的框架包括放弃识别强双相似系统，发明新的归纳原理，为进程代数开发新的公理基础，为操作语义开发新的同余格式，以及创建新的时间和概率处理方法。即使是简单的系统，如公平交换器或互斥协议，在缺乏公平性假设的情况下，也不能在标准进程代数（或Petri网）中准确地指定。因此，这项工作涉及适当的语言或模型扩展的研究，以及它们的表达能力。

2017-11-12cs.LO

确保分布式系统的活性性质：开放问题

Ensuring Liveness Properties of Distributed Systems: Open Problems

为了建立分布式系统的活性属性，通常需要进行公平性假设，但在许多情况下，它们会导致错误的结论。本文件提出了一个研究议程，旨在奠定基础的并发性理论，配备，以确保分布式系统的活性属性，而不作出公平的假设。这个理论将包括进程代数，时态逻辑和语义模型。该议程还包括开发一种方法和工具，使这一理论的规范，分析和验证的现实分布式系统的成功应用。当代进程代数和时态逻辑无法区分系统，其中一个具有关键的活性属性，另一个没有，至少在假设公正性时，强进展属性，但不假设公平性。建立一个替代的框架包括放弃识别强双相似系统，发明新的归纳原理，为进程代数开发新的公理基础，为操作语义开发新的同余格式，以及创建时间和概率的匹配处理。即使是简单的系统，如公平交换器或互斥协议，在缺乏公平性假设的情况下，也不能在标准进程代数（或Petri网）中准确地指定。因此，这项工作涉及适当的语言或模型扩展的研究，以及它们的表达能力。

2019-08-04cs.LO

关于在弱内存模型上证明活锁性的研究（扩展版本）

Towards Proving Liveness on Weak Memory (Extended Version)

本文提出了一种基于弱公平性的证明演算，用于在弱内存模型中证明活锁性，并应用于票锁算法以证明其在多种内存模型下的无饥饿性。

2026-02-23cs.LO

模态$\mu$-演算公式中的进展、公正性与公平性

Progress, Justness and Fairness in Modal $μ$-Calculus Formulae

针对模态$\mu$-演算中刻画带假设的活性属性难度高、易出错的问题，提出可实例化为多种活性属性的模板公式，覆盖进展、公正性等五类动作相关假设，且已证明公式正确性。

2024-07-10cs.LO

支持保持互模拟等价性

Enabling Preserving Bisimulation Equivalence

大多数用于验证活性属性的公平性假设都被批评为过于强大或不切实际。另一方面，公正性，可以说是验证活性属性所需的最小公平性假设，并不被经典的语义等价所保留，例如强双相似性。为了克服这一缺陷，我们引入了一个更好的替代强双相似性，使保持双相似性。我们证明了这个等价是正义的保持和所有的标准运营商，包括并行组合的一个同余。

2021-07-31cs.LO

更多相关论文收起更多论文

公正性：一个捕捉活性性质的完备性准则

Justness: A Completeness Criterion for Capturing Liveness Properties

本文提出，迁移系统构成一个很好的分布式系统模型，只有结合一个标准，告诉哪些路径模型完成运行的代表系统。在这些标准中，进展太弱，无法捕获相关的活性属性，公平性往往太强;对于典型的应用程序，我们主张公正的中间标准。以前，我们提出了一个公正的定义，在转换之间的非对称并发关系。在这里，我们定义了这样一个并发关系的过渡系统相关联的进程代数CCS以及其扩展与广播通信和信号，从而使这些进程代数适合捕捉需要公正的活性属性。

2021-08-25cs.LO

具有公平性的受保护协议的紧截止

Tight Cutoffs for Guarded Protocols with Fairness

保护协议是Emerson和Kahlon（2000）在一篇开创性的论文中介绍的，描述了进程系统，其转换的启用或禁用取决于某些局部状态下其他进程的存在。我们研究参数化模型检验和综合的保护协议，都针对系统的形式正确性参数与任何数量的进程。截断结果减少了对具有任意数量进程的系统的推理，使系统具有确定的、固定的大小。我们的工作源于观察，现有的截止结果的保护协议i）限于封闭系统，和ii）是有限的使用活性性质，因为减少不保持公平。我们关闭这些差距，并获得新的截止结果的开放系统下的公平性假设的活性。此外，我们还获得了检测全局和局部死锁的截止点，这在合成中至关重要。最后，我们证明了新的截断的紧性或渐近紧性。

2015-11-05cs.LO

进程代数中的进步、公平与公正

Progress, Fairness and Justness in Process Algebra

为了证明并发系统的活性性质，常常需要假设系统的进展性、公平性和公正性。本文探讨了如何必要的进展，公平和公正的假设可以添加到或纳入一个标准的过程代数规格说明形式主义。我们提出了一个形式化，可以应用到广泛的进程代数。所提出的形式主义是用来在无线网络的设置有关路由发现和数据包传递的原因。

2015-01-14cs.LO

公平性假设下事件系统的不动点语义

A Fixpoint Semantics of Event Systems with and without Fairness Assumptions

我们提出了一个不动点语义的事件系统。语义是在一个通用的框架，没有公平的关注。在这个一般框架中证明了推导“引导”属性的规则的合理性和完整性。一般框架实例化到最小的进展和弱公平性的假设和类似的结果。我们证明了这些结果的力量，通过推导出充分条件的“导致”在最小的进展证明健全的证明义务，而无需推理的状态痕迹。

2005-12-21cs.LO

检查公平性和行为抽象中的属性

Checking Properties within Fairness and Behavior Abstractions

本文的动机是这样一个事实，即在公平条件下验证活性属性往往是有问题的，特别是当使用抽象。它表明，在公平下使用比真理更抽象的概念，特别是在公平范围内满足的属性的概念可以导致有趣的可能性。从技术上讲，它首先建立，决定满意度内的公平是一个PSPACE-完全的问题，它表明，公平内满足的属性总是可以满足一些公平的实现。然后，研究了行为抽象与公平性满足之间的相互作用，证明了如果抽象同态是弱连续闭的，则公平性满足可以在行为抽象上得到验证.

2001-01-19cs.LO

关键软件的半自动化模块化形式验证：活性和完备性阈值

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds

本论文提出两项贡献：一是用于公平调度下忙等待程序终止性验证的分离逻辑，二是将有界内存安全证明简化为有界证明的完备性阈值概念，并刻画了数组遍历程序的阈值。

2024-03-14cs.LO

基于公平性假设的实时的系统仿真检验

Simulation-Checking of Real-Time Systems with Fairness Assumptions

研究了稠密时间系统的模拟问题。如果规范可以匹配模型在某个时间点可以进行的每个转换，则规范模拟模型。我们还采用了Emerson和Lei的方法，并在检查仿真关系时允许多个强和弱公平性假设。此外，我们允许指定为状态谓词或事件谓词的公平性假设。我们专注于一个子类的问题，最多有一个公平的假设规范。然后，我们提出了这个子类的模拟检查算法。我们提出了一个模型的模拟规范对一个共同的环境。我们提出了有效的技术，这样的模拟考虑到共同的环境。实验结果表明，这种考虑可以显著提高仿真验证的效率。我们还报告了我们的算法在检查活性与公平性假设的性能。

2010-07-04cs.LO

几乎公平的模拟

Almost Fair Simulations

CISPA Helmholtz Center for Information Security（CISPA赫尔霍夫信息安全中心）；Saarland University（萨尔兰大学）

针对带Büchi公平条件的迁移系统，提出一系列几乎公平的模拟关系，并为其配备直观推理规则，以证明公平迹包含，并在Rocq证明助手中机械化验证。

2026-05-26cs.FLcs.LO

事件系统和访问控制

Event Systems and Access Control

我们认为访问控制（权限，禁令，义务和用户权限）的概念的解释作为运行时属性的信息系统指定为事件系统的公平性。我们给出了证明规则，用于验证系统中执行的访问控制策略，并考虑通过细化事件系统来保存访问控制。特别是，细化用户的权利是不平凡的，我们建议结合低层次的用户权利和系统的义务，实现高层次的用户权利。

2006-04-21cs.CRcs.LO

单元B方法--由进度关注点引导的细化

The Unit-B Method -- Refinement Guided by Progress Concerns

我们提出了Unit-B，一个正式的方法的灵感来自事件B和UNITY。单元B旨在逐步设计满足安全性和活性特性的软件系统。该方法的特点是新的概念，粗和细的时间表，一个概括的弱和强的公平性指定事件的调度假设。基于事件时间表，我们提出了证明规则，原因的进展性质和细化顺序保持活性和安全属性。我们通过一个例子来说明我们的方法，表明系统开发不仅可以由安全性，而且还可以由活性要求来驱动。

2020-03-31cs.LOcs.SEcs.SY

用于无限状态系统的高效一阶时态逻辑

Efficient First-Order Temporal Logic for Infinite-State Systems

在本文中，我们考虑的规范和验证的无限状态系统使用时序逻辑。特别是，我们描述参数化系统使用一个新的品种的一阶时序逻辑，这是足够强大的这种形式的规范和易于处理的实际演绎验证。重要的是，时态语言的强大功能使我们能够描述（和验证）异步系统，通信延迟和更复杂的属性，如活性和公平性。这些方面对于许多其他无限状态验证方法来说似乎很困难。

2007-02-06cs.LO

保持公平：等价性

Keep it Fair: Equivalences

对于并发和分布式系统的模型，建立安全性和/或活性属性的正确性是重要的，也是具有挑战性的。分布式系统的理论认为等价性是基本的，因为它们（1）保持期望的正确性特征，（2）通常允许组件替换，使组合推理可行。分布式系统建模通常需要利用非确定性进行抽象，这会导致无限执行的非预期行为，其中一个非确定性选择被递归解决，每次忽略一个替代方案。这些情况被认为是不现实的或极不可能的。公平性假设通常用于过滤系统行为，从而区分现实和不现实的执行。这允许在分布式系统的正确性证明中使用关键参数，否则这是不可能的。我们的贡献是一个等价谱，其中公平性假设被保留。所识别的等价物允许关于结合公平性假设的正确性的（组合）推理。

2017-11-30cs.DCcs.FLcs.LO

弱内存验证的统一公平性

Unified Fairness for Weak Memory Verification

本文针对弱内存并发程序的 omega-正则活性验证，提出通用操作模型及语言理论与概率等价的统一公平性，将定性和定量验证归约为控制状态可达性。

2024-09-09cs.LOcs.PL

参数化概率并发系统的公平终止（技术报告）

Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)

我们考虑的问题，自动验证一个参数化的概率并发系统的家庭终止的概率为1的所有实例对抗对抗的竞争对手。一个参数化的族定义了一个无限状态系统：对于每个数n，这个族由一个实例和n个有限状态进程组成。与安全性相比，活性的参数化验证目前仍然被认为是极具挑战性的，特别是在模型中存在概率的情况下。一个主要的挑战是提供一个足够强大的象征性框架。一个著名的符号框架的参数化验证的非概率并发系统是定期模型检验。虽然该框架最近扩展到概率系统，将公平性的框架-通常是至关重要的验证终止-一直特别困难，由于存在无限数量的公平性约束（每个过程一个）。我们的主要贡献是一个系统的，正则保持，编码有限的公平性（一个现实的公平性的概念，提出了由Henzinger）定期模型检验的概率参数化系统的框架。我们的编码减少了终止有限的公平性，以验证参数化的终止没有公平性的概率系统在定期模型检验（验证框架已经存在）。我们表明，我们的算法可以验证终止许多有趣的例子，从分布式算法（赫尔曼的协议）和进化生物学（莫兰过程，细胞周期开关），这并不符合标准的公平概念。据我们所知，我们的算法是第一个全自动的方法，可以证明这些例子的终止。

2017-10-30cs.DCcs.FLcs.LO

会话的大协奏曲：会话的公平终止

Concerto Grosso for Sessions: Fair Termination of Sessions

本文在 Agda 中机械化推理系统元理论，研究会话类型通信中的公平终止及其与无锁性的关系。

2023-07-08cs.LOcs.PL