Expressing the Behavior of Three Very Different Concurrent Systems by Using Natural Extensions of Separation Logic
Logic in Computer Science
2009-11-12 v1 Software Engineering
Abstract
Separation Logic is a non-classical logic used to verify pointer-intensive code. In this paper, however, we show that Separation Logic, along with its natural extensions, can also be used as a specification language for concurrent-system design. To do so, we express the behavior of three very different concurrent systems: a Subway, a Stopwatch, and a 2x2 Switch. The Subway is originally implemented in LUSTRE, the Stopwatch in Esterel, and the 2x2 Switch in Bluespec.
Cite
@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}
}