Algebraic process verification. (Q2760254)

The article shows how to verify distributed and communicating systems in an effective way from an explicit process algebraic standpoint. All calculations involved are based on the axioms and principles of process algebras. The standard process algebra is extended by adding equational data types. Various means to verify complex systems are explained including: invariants, linear process operations, the cones and foci method, the use of confluence, and the composition of similar parallel processes. Verifications of the serial line interface protocol and IEEE 1394 tree identify protocol are presented as an illustration of the method.NEWLINENEWLINEFor the entire collection see [Zbl 0971.00006].