Practical methods for the formal validation of SDL specifications

Computer CommunicationsPublished 1 March 1992

Gerard J. Holzmann

DOI10.1016/0140-3664(92)90132-x

Source URL

Citations21

SJR quartileQ1

SJR score1.11

SNIP1.55

TL;DR

Some initial experience is reported on with the application of a formal validation system to SDL design projects involving more than ten people, producing tens of thousands of lines of high-level code over several years.

Abstract

Formal design and validation methods have achieved most of their successes on problems of a relatively modest size, involving no more than one or two designers and no more than a few hundred lines of code. The serious application of formal methods to larger software development projects remains a formidable challenge. In this paper we report on some initial experience with the application of a formal validation system to SDL design projects involving more than ten people, producing tens of thousands of lines of high-level code over several years. The problems encountered here are large enough for most formal methods to break down, for both technical and nontechnical reasons.

Keywords

Computer Science

Design and validation of computer protocols

1,695 Citations1991Gerard J. Holzmann

Part 1 Basic: introduction protocol structure error control flow control and design tools: a protocol simulator a protocol validator using the validator.

Software Practice and ExperienceAn improved protocol reachability analysis technique

131 Citations1988Gerard J. Holzmann

An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually.

Medical Entomology and ZoologyTelecommunications Systems Engineering Using Sdl

84 Citations1989Jared R. W. Smith, Rick Reed

Specification of Telecommunication Systems, a Fully Declarative Specification of a Telecommunication System, and Examples of Structure Representation and System Specification: Defining Sorts from First Principles.

On Limits and Possibilities of Automated Protocol Analysis

83 Citations1987Gerard J. Holzmann

A simple symbolic execution method based on vector addition is extended into a full protocol validator, carefully avoiding known performance bottlenecks and allows validation of protocol systems up to 10 6 states in only minutes of CPU time on a medium size computer.

ACM SIGCOMM Computer Communication ReviewBook Review: Design and Validation of Computer Protocols by Gerard J. Holzmann (Prentice Hall, 1991)

69 Citations1991Lars‐Åke Fredlund

The author presents the contents of a protocol specification, and describes basic rules for constructing protocols successfully, and uses reachability analysis methods to verify that a protocol satisfies each type of correctness criterion.

AT&T Technical JournalAlgorithms for Automated Protocol Verification

56 Citations1990Gerard J. Holzmann

The algorithm derived in this manner works in a fixed-size memory arena (it will never run out of memory), it is up to 2 orders of magnitude faster than the previous methods, and it has superior coverage of the state space when analyzing large protocol systems.

Computer Networks and ISDN SystemsCCITT SDL: Overview of the language and its applications

52 Citations1987Roberto Saracco, Paul A. J. Tilanus

This introductory paper gives an overview of the SDL language according to its final definition, its fields of applications and the available support tools, and makes some guesses on the future use of SDL in large industrial telecommunication environments.

Algorithms for Automated Protocol Validation

48 Citations1988Gerard J. Holzmann

This paper studies the four basic types of algorithm for the automated validation of the logical consistency of data communication protocols and finds the first for which the search efficiency does not depend of the size of the state space: there is no time penalty for analyzing very large state spaces.

Validating SDL Specifications: an Experiment

47 Citations1989Gerard J. Holzmann, Joanna Patti

A method for validating specifications written in the CCITT language SDL has been implemented as part of an experimental validation system and has been able to perform exhaustive analyses of systems with over 250 million reachable composite system states.

Tools and Rules for the Practicing Verifier

45 Citations1990Zohar Manna, Amir Pnueli

A minimal proof theory which is adequate for proving the main important temporal properties of reactive programs, and illustrates the application of these rules by analyzing and verifying the properties of a new algorithm for mutual exclusion.