In a computer network, the transport layer uses the service offered by the network layer and in turn offers its users the transport service of reliable connection management and data transfer. We provide a formal specification of the transport service in terms of an event-driven system and safety and progress properties. We construct three verified transport protocols that offer the transport service. The first transport protocol assumes a perfect network service, the second assumes loss-only network service, and the third assumes loss, reordering and duplication network service.
rnOur transport service specifications are very realistic. Each user can be closed, listening, active opening, passive opening, open, or closing. A local incarnation number uniquely identifies every active opening and listening duration. Users can issue requests for connection, listening, closing, data send, etc. The transport layer issues indications for successful or unsuccessful connection, closing, data reception, etc. A connection is established only if one user requested the connection and the other was listening, or both requested the connection. A user receives data only from the appropriate incarnation of the distant user, and receives it insequence, without loss or duplication. Progress properties ensure that every outstanding user request is eventually responded to by an appropriate transport indication.
rnOur protocols are constructed by stepwise refinement of the transport service. The construction method automatically generates a verification that the protocols satisfy the transport service. One distinctive feature of our protocol construction is that the events and verification of the data transfer function is directly obtained from any one of the numerous verified single-incarnation data transfer protocols already presented in the literature.
在计算机网络中,传输层使用网络层提供的服务,进而为用户提供可靠的连接管理和数据传输的传输服务。我们根据事件驱动系统以及安全性和进度属性提供运输服务的正式规范。我们构建了三个经过验证的提供运输服务的运输协议。第一个传输协议假设一个完美的网络服务,第二个传输协议假设一个仅丢失的网络服务,第三个假设丢失,重新排序和复制网络服务。 P> rn
我们的传输服务规范非常现实。每个用户都可以关闭,聆听,主动打开,被动打开,打开或关闭。本地化身编号唯一地标识每个活动的开放和收听持续时间。用户可以发出连接,监听,关闭,数据发送等请求。传输层会发出连接成功,失败,关闭,数据接收等指示,仅当一个用户请求连接而另一用户正在监听时才建立连接,或两者都请求连接。用户仅从遥远的用户的适当化身接收数据,并且接收数据的顺序,而不会丢失或重复。进度属性可确保最终通过适当的传输指示响应每个未完成的用户请求。 P> rn
我们的协议是通过逐步完善传输服务来构造的。构造方法会自动生成协议满足传输服务的验证。我们协议构造的一个显着特征是,可以直接从文献中已经提出的众多经过验证的单身数据传输协议中的任何一种中获取事件和数据传输功能的验证。 P>
Univ. of Maryland, College Park;
机译:传输层的连接管理:服务规范和协议验证
机译:会话协议:用于规范和验证反应式电子服务的形式主义
机译:用于规范和分析安全协议的分层游戏框架
机译:MANET上跨层覆盖P2P构造协议的正式规范和分析
机译:分层通讯协议的规范,组成和自动验证。
机译:影响空穴传输层对反型热稳定性的影响使用加速热寿命协议的有机光伏
机译:用于TCp / UDp传输上的NetBIOs服务的协议标准:详细规范
机译:计算机通信传输协议的规范。第7卷。测试OsI协议 - 论文汇编。第8卷.ICsT传输协议实施测试系统用户指南。第9卷。实施ICsT传输协议的测试套件。第10卷。用于实施ICsT传输协议的远程场景解释器的规范