- Author
- Bushby, S. T.
- Title
- Formal Analysis of the BACnet MS/TP Medium Access Control Protocol.
- Coporate
- National Institute of Standards and Technology, Gaithersburg, MD
- Sponsor
- Department of Energy, Washington, DC
- Report
- NISTIR 4777, April 1992, 25 p.
- Distribution
- Available from National Technical Information Service
- Keywords
- BACnet | building automation | CMSV | formal model | communication protocol
- Abstract
- BACnet, a draft standard communication protocol for building automation and control systems, contains options for physical and data link layer protocols. One option is to use an EIA-485 physical layer combined with a Master-Slave/Token Passing (MS/TP) media access control protocol which was specifically designed for BACnet. This paper presents a formal model of the MS/TP protocol using the technique of communicating machines with shared variables. Using this model, the protocol is analyzed and shown to be deadlock free. It is also shown that if a controller has a message to send it will eventually be transmitted.