The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - June (1987 vol.13)
pp: 683-696
G.J. Holzmann , AT& T Bell Laboratories
ABSTRACT
Argos is a validation language for data communication protocols. To validate a protocol, a model in Argos is constructed consisting of a control flow specification and a formal description of the correctness requirements. This model can be compiled into a minimized lower level description that is based on a formal model of communicating finite state machines. An automated protocol validator trace uses these minimized descriptions to perform a partial symbolic execution of the protocol to establish its correctness for the given requirements.
INDEX TERMS
symbolic execution, Assertion proving, guarded command languages, protocol design, protocol validation, scatter searching
CITATION
G.J. Holzmann, "Automated Protocol Validation in Argos: Assertion Proving and Scatter Searching", IEEE Transactions on Software Engineering, vol.13, no. 6, pp. 683-696, June 1987, doi:10.1109/TSE.1987.233206
18 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool