SAT-solving in CSP trace refinement
- 作者：Hristina Palikareva ; hristina.palikareva@cs.ox.ac.uk ; Joë ; l Ouaknine ; A.W. Roscoe
- 关键词：CSP ; FDR ; Concurrency ; Process algebra ; SAT-solving ; Bounded model checking ; k-induction ; Safety properties
- 刊名：Science of Computer Programming
- 出版年：2012
- 期刊代码：108_01676423
- 类别：cp
- 出版时间：1 September, 2012
- 卷：77
- 期：10-11
- 页码：1178-1197
- 文件大小：464 K
摘要
In this paper, we address the problem of applying SAT-based bounded model checking (BMC) and temporal -induction to asynchronous concurrent systems. We investigate refinement checking in the process-algebraic setting of Communicating Sequential Processes (CSP), focusing on the CSP traces model which is sufficient for verifying safety properties. We adapt the BMC framework to the context of CSP and the existing refinement checker FDR yielding bounded refinement checking which also lays the foundation for tailoring the -induction technique. As refinement checking reduces to checking for reverse containment of possible behaviours, we exploit the SAT-solver to decide bounded language inclusion as opposed to bounded reachability of error states, as in most existing model checkers. Due to the harder problem to decide and the presence of invisible silent actions in process algebras, the original syntactic translation of BMC to SAT cannot be applied directly and we adopt a semantic translation algorithm based on watchdog transformations. We propose a Boolean encoding of CSP processes resting on FDR鈥檚 hybrid two-level approach for calculating the operational semantics using supercombinators. We have implemented a prototype tool, SymFDR, written in C++, which uses FDR as a shared library for manipulating CSP processes and the state-of-the-art incremental SAT-solver MiniSAT聽2.0. Experiments with BMC indicate that in some cases, especially in complex combinatorial problems, SymFDR significantly outperforms FDR and even copes with problems that are beyond FDR鈥檚 capabilities. SymFDR in -induction mode works reasonably well for small test cases, but is inefficient for larger ones as the threshold becomes too large, due to concurrency.