Verification ot Distributed Applications by translating CCS to Binary Decision Diagrams

摘要

Process algebras describe systems as a composition of processes, synchronized by common actions. Correctness is proven by establishing a bisimulation equivalence between the implementation model and a reference specification, or by model checking with Hennessy-Milner-fomulas. This task can be supported by suitable software tools, such as the well known Concurrency Workbench (CWB) [2] for the CCS calculus. However, automated proofs often fail due to the complexity of real systems which lead to huge state spaces. An alternative are representations as Binary Decision Diagrams (BDDs) because BDD-representations are substantially more compact than other forms. In this paper we apply this technique to the verification of process algebraic specifications and thereby demonstrate its advantages over LTS-based verification techniques.