Many distributed systems rely on token structures for their correct operation. Often, these structures make sure that a fixed number of tokens exists at all times, or perhaps that tokens cannot be completely eliminated, to prevent systems from reaching undesired states. In this paper we show how a SAT checker can be used to automatically detect token and similar invariants in distributed systems, and how these invariants can improve the precision of a deadlock-checking framework that is based on local analysis. We demonstrate by a series of practical experiments that this new framework is as efficient as similar incomplete techniques for deadlock-freedom analysis, while handling a different class of systems.
CITATION STYLE
Antonino, P., Gibson-Robinson, T., & Roscoe, A. W. (2017). The automatic detection of token structures and invariants using SAT checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10206 LNCS, pp. 249–265). Springer Verlag. https://doi.org/10.1007/978-3-662-54580-5_15
Mendeley helps you to discover research relevant for your work.