使用FASE自动分析MUTEX算法
计算机科学中的逻辑
2011-06-08 v1
摘要
在本文中，我们通过将几种MUTEX解决方案表示为PAFASs中的进程来研究其活性，PAFASs是一种类似CCS的进程代数，具有用于建模非阻塞读取行为的特定算子。利用工具FASE进行验证，利用了活性属性的违反与某个转移系统中的一种特殊循环（称为灾难性循环）之间的对应关系。我们还将我们的方法与文献中的其他方法进行了比较。本文的目的有两个：一方面，我们想要展示FASE在一些具体且有意义的示例上的适用性；另一方面，我们想要研究在建模并发系统中引入非阻塞行为的影响。
引用
@article{arxiv.1106.1231,
title = {Automated Analysis of MUTEX Algorithms with FASE},
author = {Federico Buti and Massimo Callisto De Donato and Flavio Corradini and Maria Rita Di Berardini and Walter Vogler},
journal= {arXiv preprint arXiv:1106.1231},
year = {2011}
}
备注
In Proceedings GandALF 2011, arXiv:1106.0814