A relational notation for state transition systems
- 1 July 1990
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 16 (7) , 755-775
- https://doi.org/10.1109/32.56101
Abstract
A relational notation for specifying state transition systems is presented. Several refinement relations between specifications are defined. To illustrate the concepts and methods, three specifications of the alternating-bit protocol are given. The theory is applied to explain auxiliary variables. Other applications of the theory to protocol verification, composition, and conversion are discussed. The approach is compared with previously published approaches.Keywords
This publication has 22 references indexed in Scilit:
- Specifying modules to satisfy interfaces: A state transition system approachDistributed Computing, 1992
- Verified data transfer protocols with variable flow controlACM Transactions on Computer Systems, 1989
- A simple approach to specifying concurrent systemsCommunications of the ACM, 1989
- Protocol conversionIEEE Transactions on Software Engineering, 1988
- Time-dependent distributed systems: proving safety, liveness and real-time propertiesDistributed Computing, 1987
- What it means for a concurrent program to satisfy a specificationPublished by Association for Computing Machinery (ACM) ,1985
- Protocol Verification via ProjectionsIEEE Transactions on Software Engineering, 1984
- An HDLC protocol specification and its verification using image protocolsACM Transactions on Computer Systems, 1983
- Specifying Concurrent Program ModulesACM Transactions on Programming Languages and Systems, 1983
- General Technique for Communications Protocol ValidationIBM Journal of Research and Development, 1978