This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Automated Protocol Validation in Argos: Assertion Proving and Scatter Searching
June 1987 (vol. 13 no. 6)
pp. 683-696
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.
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
Usage of this product signifies your acceptance of the Terms of Use.