[go: up one dir, main page]

Gebremichael et al., 2006 - Google Patents

Analysis of the Zeroconf protocol using Uppaal

Gebremichael et al., 2006

View PDF
Document ID
17671911721052444715
Author
Gebremichael B
Vaandrager F
Zhang M
Publication year
Publication venue
Proceedings of the 6th ACM & IEEE International conference on Embedded software

External Links

Snippet

We report on a case study in which the model checker Uppaal is used to formally model parts of Zeroconf, a protocol for dynamic configuration of IPv4 link-local addresses that has been defined in RFC 3927 of the IETF. Our goal has been to construct a model that (a) is …
Continue reading at sws.cs.ru.nl (PDF) (other versions)

Classifications

    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L29/00—Arrangements, apparatus, circuits or systems, not covered by a single one of groups H04L1/00 - H04L27/00 contains provisionally no documents
    • H04L29/12—Arrangements, apparatus, circuits or systems, not covered by a single one of groups H04L1/00 - H04L27/00 contains provisionally no documents characterised by the data terminal contains provisionally no documents
    • H04L29/12009—Arrangements for addressing and naming in data networks
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L12/00—Data switching networks
    • H04L12/02—Details
    • H04L12/26—Monitoring arrangements; Testing arrangements
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L29/00—Arrangements, apparatus, circuits or systems, not covered by a single one of groups H04L1/00 - H04L27/00 contains provisionally no documents
    • H04L29/02—Communication control; Communication processing contains provisionally no documents
    • H04L29/06—Communication control; Communication processing contains provisionally no documents characterised by a protocol
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L41/00—Arrangements for maintenance or administration or management of packet switching networks
    • H04L41/12—Arrangements for maintenance or administration or management of packet switching networks network topology discovery or management
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/46—Multiprogramming arrangements
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L12/00—Data switching networks
    • H04L12/28—Data switching networks characterised by path configuration, e.g. local area networks [LAN], wide area networks [WAN]
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L41/00—Arrangements for maintenance or administration or management of packet switching networks
    • H04L41/02—Arrangements for maintenance or administration or management of packet switching networks involving integration or standardization
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/07—Error detection; Error correction; Monitoring responding to the occurence of a fault, e.g. fault tolerance
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L61/00—Network arrangements or network protocols for addressing or naming
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L63/00—Network architectures or network communication protocols for network security
    • H04L63/14—Network architectures or network communication protocols for network security for detecting or protecting against malicious traffic
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L43/00—Arrangements for monitoring or testing packet switching networks
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L69/00—Application independent communication protocol aspects or techniques in packet data networks
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity

Similar Documents

Publication Publication Date Title
US7149678B2 (en) High level executable network abstract machine
Willcock et al. An introduction to TTCN-3
CN109067930A (en) Domain name cut-in method, domain name analytic method, server, terminal and storage medium
US20080288470A1 (en) Method and System for Distributed Dns Resolution
Gebremichael et al. Analysis of the Zeroconf protocol using Uppaal
Sidhu et al. Experience with formal methods in protocol development
Shankland et al. The tree identify protocol of IEEE 1394 in μCRL
Gebremichael et al. Analysis of a protocol for dynamic configuration of IPv4 link local addresses using Uppaal
Saad-Khorchef et al. A framework and a tool for robustness testing of communicating software
Küsters et al. Computational soundness for key exchange protocols with symmetric encryption
Berendsen et al. Formal specification and analysis of zeroconf using uppaalS
Jørgensen et al. Modelling and analysis of distributed program execution in BETA using coloured Petri nets
Hendriks Model checking the time to reach agreement
Glässer et al. Universal Plug and Play Machine Models.
Gebremichael-Tesfagiorgis et al. Analysis of the Zeroconf Protocol using Uppaal
Gebremichael-Tesfagiorgis et al. Analysis of a Protocol for Dynamic Configuration of IPv4 Link Local Addresses Using Uppaal
CN116627689A (en) Chaos Engineering Platform and Fault Injection Method Supporting Mixed Orchestration of Multiple Injection Objects
Berendsen et al. Formal specification and analysis of zeroconf using Uppaal
CN110266554A (en) A kind of test method of privately owned communication protocol
Rothmaier et al. Using Spin and Eclipse for optimized high-level modeling and analysis of computer network attack models
Liu et al. User behavior simulation in ICS cyber ranges
Gallasch et al. Checking safety properties on-the-fly with the sweep-line method
Ramsokul et al. Aseha: A framework for modelling and verification ofweb services protocols
Griffeth et al. Testing a network by inferring representative state machines from network traces
CN114465986B (en) IP address conflict processing method, electronic device, and computer-readable storage medium