Analysing properties of the resource reservation protocol
作者： María E. Villapol , Jonathan Billington
关键词: Host (network) 、 Router 、 Computer science 、 Graph (abstract data type) 、 Protocol (object-oriented programming) 、 The Internet 、 Quality of service 、 Internet Protocol 、 Distributed computing 、 Resource Reservation Protocol 、 Petri net
摘要: The goal of the Resource Reservation Protocol (RSVP) is to establish Quality Service information within routers and host computers Internet. This paper describes a model RSVP presents analysis approach results. A large part modelled using Coloured Petri Nets. provides clear, unambiguous precise definition considered features RSVP, which missing in current protocol specification. analysed for set general properties, such as correct termination, specific properties defined this paper. are checked by querying state graph its associated strongly connected component graph. As first step, we analyse under assumption perfect medium ensure that errors not hidden rare events medium. results show satisfies properties.
springer.com
sci-hub.st 参考文章(18)
M. A. S. Smith, Formal verification of communication protocols formal techniques for (networked and) distributed systems. pp. 129- 144 ,(1996) , 10.1007/978-0-387-35079-0_8
Raj Yavatkar, David Durham, Inside the Internet's Resource reSerVation Protocol: Foundations for Quality of Service ,(1999)
Laurence C. Paulson, ML for the working programmer ,(1991)
Chun Ouyang, Lars Michael Kristensen, Jonathan Billington, A Formal and Executable Specification of the Internet Open Trading Protocol electronic commerce and web technologies. pp. 377- 387 ,(2002) , 10.1007/3-540-45705-4_39
S. J. Creese, Joy Reed, Verifying End-to-End Protocols using Induction with CSP/FDR international parallel processing symposium. pp. 1243- 1257 ,(1999) , 10.1007/BFB0098006
Kurt Jensen, Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use ,(2011)
Grzegorz Rozenberg, Jonathan Billington, Michel Diaz, Application of Petri Nets to Communication Networks: Advances in Petri Nets ,(1999)
JN Reed, DM Jackson, B Deianov, GM Reed, Automated formal analysis of networks : FDR models of arbitrary topologies and flow-control mechanisms fundamental approaches to software engineering. pp. 239- 254 ,(1998) , 10.1007/BFB0053594
K. Jensen, Coloured Petri nets Discrete Event Systems: A New Challenge for Intelligent Control Systems, IEE Colloquium on. ,(1993)
Jonathan Billington, Bing Han, Validating TCP connection management formal methods. pp. 47- 55 ,(2002)