Reasoning about Protocols using Dijkstra’s Calculus

A mathematical model for the specification and verification of a data link layer protocol is proposed. The weakest precondition calculus, developed by Dijkstra, originally for sequential programs, has been chosen for this purpose. It is demonstrated that the wp-calculus provides a basis, not only fo...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Singh, Awadhesh Kumar, Bandyopadhyay, Anup Kumar
Formato: Articulo
Lenguaje:Inglés
Publicado: 2004
Materias:
Ciencias Informáticas
weakest precondition
correctness
Specifying and Verifying and Reasoning about Programs
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/9476
http://journal.info.unlp.edu.ar/wp-content/uploads/JCST-Apr04-4.pdf
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-9476
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
weakest precondition
correctness
Specifying and Verifying and Reasoning about Programs
spellingShingle Ciencias Informáticas
weakest precondition
correctness
Specifying and Verifying and Reasoning about Programs
Singh, Awadhesh Kumar
Bandyopadhyay, Anup Kumar
Reasoning about Protocols using Dijkstra’s Calculus
topic_facet Ciencias Informáticas
weakest precondition
correctness
Specifying and Verifying and Reasoning about Programs
description A mathematical model for the specification and verification of a data link layer protocol is proposed. The weakest precondition calculus, developed by Dijkstra, originally for sequential programs, has been chosen for this purpose. It is demonstrated that the wp-calculus provides a basis, not only for the modeling but also, for a straightforward and thorough analysis of large and complex distributed systems like data link layer protocol. This analysis contributes to the understanding of the system and could lead to an improvement in the design. The technique has been illustrated by describing the sliding window protocol.
format Articulo
Articulo
author Singh, Awadhesh Kumar
Bandyopadhyay, Anup Kumar
author_facet Singh, Awadhesh Kumar
Bandyopadhyay, Anup Kumar
author_sort Singh, Awadhesh Kumar
title Reasoning about Protocols using Dijkstra’s Calculus
title_short Reasoning about Protocols using Dijkstra’s Calculus
title_full Reasoning about Protocols using Dijkstra’s Calculus
title_fullStr Reasoning about Protocols using Dijkstra’s Calculus
title_full_unstemmed Reasoning about Protocols using Dijkstra’s Calculus
title_sort reasoning about protocols using dijkstra’s calculus
publishDate 2004
url http://sedici.unlp.edu.ar/handle/10915/9476
http://journal.info.unlp.edu.ar/wp-content/uploads/JCST-Apr04-4.pdf
work_keys_str_mv AT singhawadheshkumar reasoningaboutprotocolsusingdijkstrascalculus
AT bandyopadhyayanupkumar reasoningaboutprotocolsusingdijkstrascalculus
bdutipo_str Repositorios
_version_ 1764820491861753856

Ejemplares similares