Mushroom: a program for the automated verification of an SCM protocol specification

Author

Lundy, G.M. ; Bulbul, B.

Author_Institution

Dept. of Comput. Sci., US Naval Postgraduate Sch., Monterey, CA, USA

fYear

1993

fDate

19-22 Oct 1993

Firstpage

272

Lastpage

279

Abstract

Systems of communicating machines (SCM) is a formal model for the specification, verification and testing of communication protocols, which has been used to specify and verify several well-known protocols. The authors discuss a program, called mushroom, which automates the analysis using the SCM model. The program generates either the system state analysis or the full reachability analysis. The automation of this model is expected to greatly facilitate the use of the model for protocol design and analysis. The program has been used to verify some theoretical results, serving to confirm these earlier results

Keywords

automatic testing; conformance testing; formal specification; formal verification; protocols; SCM model; SCM protocol specification; automated verification; communication protocols; finite state machines; formal model; mushroom; protocol analysis; protocol design; protocol testing; protocol verification; reachability analysis; system of communicating machines; system state analysis; Automata; Computer networks; Government; Protection; Protocols; Reachability analysis; Standardization; System testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Network Protocols, 1993. Proceedings., 1993 International Conference on

Conference_Location

San Francisco, CA

Print_ISBN

0-8186-3670-X

Type

conf

DOI

10.1109/ICNP.1993.340910

Filename

340910