Issue No. 06 - June (1987 vol. 13)
G.J. Holzmann , AT& T Bell Laboratories
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.
symbolic execution, Assertion proving, guarded command languages, protocol design, protocol validation, scatter searching
G. Holzmann, "Automated Protocol Validation in Argos: Assertion Proving and Scatter Searching," in IEEE Transactions on Software Engineering, vol. 13, no. , pp. 683-696, 1987.