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.
No takes yet. Share an insight, caveat, or question.
Gerard J. Holzmann (1987) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: