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

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 o...

Full description

Autores:

Rocha, Camilo
Meseguer, José

Tipo de recurso:

Part of book

Fecha de publicación:

2014

Institución:

Escuela Colombiana de Ingeniería Julio Garavito

Repositorio:

Repositorio Institucional ECI

Idioma:

eng

OAI Identifier:

oai:repositorio.escuelaing.edu.co:001/1882

Acceso en línea:

https://repositorio.escuelaing.edu.co/handle/001/1882

Palabra clave:

Comprobación del modelo
Regla de inferencia
Propiedad de seguridad
Flujo de entrada
Obligación de prueba
Model Check
Inference Rule
Safety Property
Input Stream
Proof Obligation

Rights

closedAccess

License

© Springer-Verlag Berlin Heidelberg 2014