Search

In this paper, we address the problem of applying SAT-based bounded model checking (BMC) and temporal k-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 k-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’s 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’s capabilities. SymFDR in k-induction mode works reasonably well for small test cases, but is inefficient for larger ones as the threshold becomes too large, due to concurrency.

One of the attractive features of occam is the large number of memorable algebraic laws which exist relating programs. We investigate these laws and, by discovering a normal form for WHILE-free programs, show that they completely characterise the language's semantics.

We study 2- and 3-dimensional digital geometry in the context of almost arbitrary adjacency relations. (Previous authors have based their work on particular adjacency relations.) We define a binary digital picture to be a pair whose components are a set of lattice-points and an adjacency relation on the whole lattice. We show how a wide class of digital pictures have natural "continuous analogs." This enables us to use methods of continuous topology in studying digital pictures. We are able to prove general results on the connectivity of digital borders, which generalize results that have appeared in the literature. In the 3-dimensional case we consider the possibility of using a uniform relation on the whole lattice. (In the past authors have used different types of adjacency for "object" and "background.") �9 1985 Academic Press, Inc. PREREQUISITES