NDLI: Specification and verification of collusion-free broadcast networks

Content Provider	ACM Digital Library
Author	Lam, S. S. Jain, P.
Abstract	For high-speed local area networks that offer integrated services for data, voice, and image traffic, a class of demand-assigned multiple-access protocols have been presented in the literature. These protocols exploit the directionality of signal propagation and enforce time constraints to achieve collision-freedom. A correct implementation of such a protocol requires a careful analysis of time-dependent interactions of event occurrences using a formal method. To date, most protocol verification methods are intended for the analysis of asynchronous communication over point-to-point channels.We present a model for broadcast bus networks. The novel features of our model include the ability to specify broadcast channels and the specification of real-time behavior. The broadcast characteristics of cables or buses are captured by some simple axioms. Real time is modeled as a discrete quantity using clocks and time variables. Real-time properties are specified by safety assertions. To illustrate our model and analysis method, we present a specification of the Expressnet protocol. We found that to achieve collision-freedom, a small modification to the original Expressnet protocol is needed.
Starting Page	282
Ending Page	291
Page Count	10
File Format	PDF
ISSN	01464833
DOI	10.1145/52325.52353
Journal	ACM SIGCOMM Computer Communication Review (CCRV)
Volume Number	18
Issue Number	4
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1993-07-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article
Subject	Computer Networks and Communications Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Specification and verification of collusion-free broadcast networks

Specification and verification of network managers for large internets

Formal specification and verification of a connection establishment protocol

Alternative specification and verification of a periodic state exchange protocol

Analysis of reliable broadcast in local-area networks

Alternative specification and verification of a periodic state exchange protocol

Simulation studies of the behavior of multihop broadcast networks

Specification and verification of an HDLC protocol with arm connection management and full-duplex data transfer

Performance analysis of a broadcast communications protocol

Specification and verification of collusion-free broadcast networks

Similar Documents

Specification and verification of collusion-free broadcast networks

Specification and verification of network managers for large internets

Formal specification and verification of a connection establishment protocol

Alternative specification and verification of a periodic state exchange protocol

Analysis of reliable broadcast in local-area networks

Alternative specification and verification of a periodic state exchange protocol

Simulation studies of the behavior of multihop broadcast networks

Specification and verification of an HDLC protocol with arm connection management and full-duplex data transfer

Performance analysis of a broadcast communications protocol

Specification and verification of collusion-free broadcast networks