弱公平性下 liveness 属性的规范与细化验证义务
计算机科学中的逻辑
2007-05-23 v1
摘要
本报告中，我们提出了B事件系统公平迭代事件的形式模型。该模型用于为基本存活属性及其在细化下的保留提供验证义务。公平事件迭代的模型使用dovetail算子，该算子由Broy和Nelson提出以建模公平选择。证明主要基于公平事件迭代的固定点计算和最弱前置条件计算。
引用
@article{arxiv.cs/0502046,
title = {Proof obligations for specification and refinement of liveness properties under weak fairness},
author = {Hector Ruiz Barradas and Didier Bert},
journal= {arXiv preprint arXiv:cs/0502046},
year = {2007}
}