Map
Index
Random
Help
th

QuoteRef: bishS1_2006




Topic:
communication protocols
Group:
program proving
Topic:
model checker
Topic:
constructing proof and program together
Topic:
state machine
Topic:
timestamps
Topic:
bugs
Topic:
reliable communication

Reference

Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K., "Engineering with Logic: HOL specification and symbolic-evaluation testing for TCP implementations", Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2006, Charleston, South Carolina, USA, January 2006, ACM SIGPLAN, 41, 1, January 2006, pp. 55-66. Google

Other Reference

Bishop,S., et al, "Transport II: Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets," Proceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications SIGCOMM '05, August 2005, ACM Press.

Quotations
abstract ;;Quote: rigorous, detailed, readable specification from real-world traces of three implementations of the TCP/IP protocols and Sockets API; verified with a symbolic model checker
57 ;;Quote: define TCP/IP and Sockets with a host labeled transition system; operational semantics, flat definition, few transition premises, no parallel composition, no internal synchronization
59 ;;Quote: distributed appications generally require timeouts for asynchronous communcation and failures; e.g., TCP
64 ;;Quote: validated a TCP/IP/Socket specification by model checking actual traces; 97% success for UDP and 91% success for TCP; half of the TCP failures due to test and check problems
64 ;;Quote: experimentally derived protocols for TCP/IP and Sockets identified many behavioural anomalies and explicit OS version dependencies

Related Topics up

Topic: communication protocols (62 items)
Group: program proving   (10 topics, 311 quotes)
Topic: model checker (49 items)
Topic: constructing proof and program together (22 items)
Topic: state machine (67 items)
Topic: timestamps (19 items)
Topic: bugs (66 items)
Topic: reliable communication (29 items)

Collected barberCB 3/06
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.