Protocol verification using discrete-event systems
- 24 August 2005
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 3770-3777
- https://doi.org/10.1109/cdc.1992.370955
Abstract
It can be shown that the problem of reliable transmission of data over an unreliable communication channel can be restated as a decentralized control problem of discrete-event systems. Necessary and sufficient conditions for the existence of solutions to such decentralized supervisory control problems have been found. These conditions are used to verify the correctness of a protocol for the data transmission problem. In particular, it is demonstrated that the authors' method provides a systematic check on whether the protocol satisfies the required safety property, as opposed to relying on finding, ad hoc, circumstances under which the protocol fails.Keywords
This publication has 10 references indexed in Scilit:
- Think globally, act locally: decentralized supervisory controlIEEE Transactions on Automatic Control, 1992
- Supervisory control of discrete-event processes with partial observationsIEEE Transactions on Automatic Control, 1988
- On the Supremal Controllable Sublanguage of a Given LanguageSIAM Journal on Control and Optimization, 1987
- Supervisory Control of a Class of Discrete Event ProcessesSIAM Journal on Control and Optimization, 1987
- Modular Verification of Computer Communication ProtocolsIEEE Transactions on Communications, 1983
- Supervision of discrete event processesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982
- Towards Analyzing and Synthesizing ProtocolsIEEE Transactions on Communications, 1980
- Formal Methods in Communication Protocol DesignIEEE Transactions on Communications, 1980
- Finite state description of communication protocolsComputer Networks (1976), 1978
- General Technique for Communications Protocol ValidationIBM Journal of Research and Development, 1978