Protocol Specification and Verification Using Process Algebra and Petri Nets

The paper deals with the issue of the verification of communication protocols based on integration of formal methods chosen (a process algebra and Petri nets). A method is proposed, that uses the process algebra for protocol specification, and transformation rules for a translation of the specification into a Petri net while preserving the semantics of the specification. Petri nets are well-known formal method for their analytical power to deal with a problem of protocol verification: invariant, reachability, deadlock and liveness analysis. Elements of theory behind the method are sketched in a short way. The elegance of protocol specification by using the process algebra and a powerful analysis by means of Petri nets are main reasons for such the integration, what is demonstrated in the paper. The method is illuminated by an example: simple data link layer network protocol known as Alternating bit protocol (ABP).