利用分离逻辑的自然扩展表达三种迥异并发系统的行为
计算机科学中的逻辑
2009-11-12 v1 软件工程
摘要
分离逻辑是一种用于验证指针密集型代码的非经典逻辑。然而，在本文中，我们展示了分离逻辑及其自然扩展也可以用作并发系统设计的规约语言。为此，我们表达了三种迥异并发系统的行为：地铁系统、秒表和2x2交换机。地铁系统最初用LUSTRE实现，秒表用Esterel实现，2x2交换机用Bluespec实现。
引用
@article{arxiv.0911.2034,
title = {Expressing the Behavior of Three Very Different Concurrent Systems by Using Natural Extensions of Separation Logic},
author = {Edgar G. Daylight and Sandeep K. Shukla and Davide Sergio},
journal= {arXiv preprint arXiv:0911.2034},
year = {2009}
}