Protocol Verifications

Abstract

Chapters 2-5 presented a standard framework ACPT τ with guarded linear recursion for the specification and manipulation of concurrent processes. Summarising, it consists of basic operators (A, +, •) to define finite processes, communication operators (|| ‖ |) to express parallelism, deadlock and encapsulation (δ, ∂ _H ) to force atomic actions into communication, silent step and abstraction (τ, τ _I ) to make internal computations invisible, and guarded linear recursion ((X|E>) to capture regular processes. These constructs form a solid basis for the analysis of a wide range of systems.