Specification of the MIL-Standard 1553 protocol using systems of communicating machines

A model for the specification and analysis of communication protocols is used to describe and analyze a simplified version of the MIL-Standard 1553 bus protocol, which does not contain an equivalent specification using a formally defined model. The protocol is used in various military aircraft for digital communication between aircraft subsystems. The model, which uses a combination of finite state machines and variables in the specification of the bus controller and remote terminals, is described. The commands and responses on the bus are accomplished through shared variables which represent the bus. Enabling predicates and actions are associated with each transition. The enabling predicates determine when a transition may be taken, and the actions alter the variable values as transitions occur. Normal, error-free 1553 bus command/response information transfers are modeled