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

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.

Actions (login required)

View Item