Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool

Abstract

The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a formula to inductive properties of the underlying equational theory by means of the application of a few inference rules. Through the combination of various techniques such as unification, narrowing, equationally-defined equality predicates, and SMT solving, InvA achieves a significant degree of automation, verifying automatically many proof obligations. Maude Inductive Theorem Prover (ITP) can be used to discharge the remaining obligations which are not automatically verified by InvA. Verification of the reliable communication ensured by the Alternating Bit Protocol (ABP) is used as a case study to explain the use of the InvA tool, and to illustrate its effectiveness and degree of automation in a concrete way.

La herramienta InvA admite la verificación deductiva de las propiedades de seguridad de los sistemas concurrentes de estado infinito. Dado un sistema concurrente especificado como una teoría de reescritura y una fórmula de seguridad a verificar, InvA reduce dicha fórmula a las propiedades inductivas de la teoría ecuacional subyacente mediante la aplicación de algunas reglas de inferencia. A través de la combinación de varias técnicas, como la unificación, el estrechamiento, los predicados de igualdad definidos por ecuaciones y la resolución SMT, InvA logra un grado significativo de automatización, verificando automáticamente muchas obligaciones de prueba. El probador del teorema inductivo de Maude (ITP) se puede utilizar para cumplir con las obligaciones restantes que InvA no verifica automáticamente. La verificación de la comunicación confiable asegurada por el Alternating Bit Protocol (ABP) se utiliza como caso de estudio para explicar el uso de la herramienta InvA, y para ilustrar su efectividad y grado de automatización de manera concreta.