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

[img]
Preview
Text
WP-80-060.pdf

Download (561kB) | Preview

Abstract

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: 23 Jul 2016 07:33
URI: http://pure.iiasa.ac.at/1409

Actions (login required)

View Item View Item

International Institute for Applied Systems Analysis (IIASA)
Schlossplatz 1, A-2361 Laxenburg, Austria
Phone: (+43 2236) 807 0 Fax:(+43 2236) 71 313