On the Specification and Verification of Communication Protocols

Petrenko, A. (1980). On the Specification and Verification of Communication Protocols. IIASA Working Paper. IIASA, Laxenburg, Austria: WP-80-060

[thumbnail of WP-80-060.pdf]

Download (561kB) | Preview


The purpose of this paper is to consider the most complicated problem related to computer network design, and especially to the so-called "gateways": the definition and estimation of the logical correctness of protocols. While the simple terminal connection of a computer to a computer system necessitates only the emulation of the chosen terminal, the very complicated interconnection of several computer networks requires the definition and implementation of a whole hierarchy of protocols. Naturally, all the protocols of each level must be rigorously specified and carefully verified before being implemented into soft-, firm-, or hardware. In order to achieve this goal, a technique based on a top-down approach, involving stepwise refinement and verification of the protocol actions in various situations, is proposed in this paper. This technique requires the formalism of a special kind of Petri net: the Petri net with enabling predicates.

Item Type: Monograph (IIASA Working Paper)
Research Programs: General Research (GEN)
Depositing User: IIASA Import
Date Deposited: 15 Jan 2016 01:48
Last Modified: 27 Aug 2021 17:09
URI: https://pure.iiasa.ac.at/1409

Actions (login required)

View Item View Item