Automated verifications of communication protocols using CCS and BDDs

The application of formal methods in protocol verification is of great importance, especially in the area of safety critical systems. Formal methods, however, are scarcely used in industrial practice today because they are hardly to integrate into the conventional system design and require a high effort in computing. We describe the implementation and application of a tool that handles formal specifications written in the process calculus CCS. The automatic verification process is based on binary decision diagrams to efficiently cope with state explosion problems. As an verification example we use a model of the CSMA/CD protocol including propagation delay effects on the transmission medium.