This Article 
 Bibliographic References 
 Add to: 
A Relational Notation for State Transition Systems
July 1990 (vol. 16 no. 7)
pp. 755-775

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.

[1] M. Abadi and L. Lamport, "The existence of refinement mappings," Digital Systems Research Center, Palo Alto, CA, Tech. Rep., Aug. 1988.
[2] CCITT,Recommendations Z.101 to Z.104. Red Book. Geneva, 1985 (Standard Definition Language).
[3] K. L. Calvert and S. S. Lam, "Formal methods for protocol conversion,"IEEE J. Select. Areas Commun., vol. 8, no. 1, Jan. 1990.
[4] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley, 1988.
[5] E. A. Emerson and E. Clarke, "Design and synthesis of synchronization skeletons using branching-time temporal logic," inProc. Workshop Logic of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, 1981.
[6] B. Hailpern and S. Owicki, "Modular verification of computer communication protocols,"IEEE Trans. Comm., vol. COM-31, Jan. 1983.
[7] E. C. R. Hehner, "Predicative programming, Part 1,"Commun. ACM, vol. 27, no. 2, pp. 134-143, Feb. 1984.
[8] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[9] IBM Corp.,Systems Network Architecture Format and Protocol Reference Manual: Architecture Logic, IBM Form No. SC32-3112-2, 1980.
[10] Estelle--A Formal Description Technique Based on an Extended State Transition Model, ISO/TC97/SC21/WGI6-1 N422, Feb. 1985.
[11] S. S. Lam, "Protocol conversion,"IEEE Trans. Software Eng., vol. 14, no. 3, Mar. 1988.
[12] S. S. Lam and A. U. Shankar, "Protocol verification via projections,"IEEE Trans. Software Eng., vol. SE-10, no. 4, July 1984.
[13] S. Lam and A. U. Shankar, "Specifying modules to satisfy interfaces: A state transition system approach," Tech. Rep. TR-88-30, Univ. of Texas at Austin, Aug. 1988. (Revised Sept. 1990).
[14] L. Lamport, "What good is temporal logic?" inProc. Information Processing 83, IFIP, 1983.
[15] L. Lamport, "Specifying Concurrent ProgramModules,"ACM Trans. Programming Languages and Systems, Vol. 5, No. 2, Apr. 1983, pp. 190-222.
[16] L. Lamport, "What it means for a concurrent program to satisfy a specification: Why no one has specified priority," inProc. 12th ACM Symp. Principles of Programming Languages, New Orleans, LA, Jan. 1985.
[17] L. Lamport, "A simple approach to specifying concurrent systems,"Commun. ACM, vol. 32, pp. 32-45, 1989.
[18] N. Lynch and M. R. Tuttle, "Hierarchical correctness proofs for distributed algorithms," inProc. Sixth Annu. ACM Symp. Principles of Distrib. Comput., 1987, pp. 137-151.
[19] Z. Manna and A. Pnueli, "Adequate proof principles for invariance and liveness properties of concurrent programs,"Sci. Comput. Program., vol. 4, pp. 257-289, 1984.
[20] Z. Manna and R. Waldinger,The Logical Basis for Computer Programming, vol. 1,Deductive Reasoning. Reading, MA: Addison-Wesley, 1985.
[21] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[22] S. L. Murphy and A. U. Shankar, "A verified connection management protocol for the transport layer," inProc. ACM SIGCOMM '87 Workshop, Stowe, VT, Aug. 1987.
[23] S. L. Murphy and A. U. Shankar, "Service specification and protocol construction for the transport layer," inProc. ACM SIGCOMM '88 Symp., Stanford Univ., Aug. 1988.
[24] S. Owicki and D. Gries, "Verifying properties of parallel programs: An axiomatic approach,"Commun. ACM, vol. 19, pp. 279-285, May 1976.
[25] Owicki, S., and L. Lamport, "Proving Liveness Properties of Concurrent Programs,"ACM Trans. Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 455-495.
[26] T. Piatkowski, "The state of the art in protocol engineering," inProc. ACM Commun. Architectures Protocols, Aug. 1986, pp. 13-18.
[27] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of CurrentTrends," inCurrent Trends in Concurrency: Overviews and Tutorials. W.-P. de Roever and G. Rozenberg, eds., Lecture Notes in Computer Science 224, Springer-Verlag, N.Y., 1986, pp. 510-584.
[28] K. Sabnani, "An algorithmic procedure for protocol verification,"IEEE Trans. Commun., vol. 36, no. 8, Aug. 1988.
[29] J. Scheid and S. Holtsberg,Ina Jo Specification Language Reference Manual, System Development Group, Unisys Corp., Santa Monica, CA, Sept. 1988.
[30] A. U. Shankar, "Verified data transfer protocols with variable flow control,"ACM Trans, Comput. Syst., vol. 7, no. 3, Aug. 1989; an abbreviated version appears inProc. ACM SIGCOMM '86, Stowe, VT, Aug. 1986.
[31] A. U. Shankar and S. S. Lam, "An HDLC protocol specification and its verification using image protocols,"ACM Trans. Comput. Syst., vol. 1, no. 4, pp. 321-368, Nov. 1983.
[32] A. U. Shankar and S. S. Lam, "Time-dependent communication protocols," inTutorial: Principles of Communication and Networking Protocols, S. S. Lam, Ed. Washington, DC: IEEE Computer Society, 1984.
[33] A. U. Shankar and S. S. Lam, "Time-dependent distributed systems: Proving safety, liveness, and real-time properties,"Distributed Comput., vol. 2, no. 2, 1987.
[34] A. U. Shankar and S. S. Lam, "A stepwise refinement heuristic for protocol construction," Dep. Comput. Sci., Univ. Maryland, Tech. Rep. CS-TR-1812, Mar. 1987 (revised Mar. 1989).
[35] C. H. West, "A general technique for communications protocol validation,"IBM J. Res. Develop., vol. 22, July 1978.

Index Terms:
relational notation; specifying state transition systems; refinement relations; alternating-bit protocol; composition; formal specification; protocols.
S.S. Lam, A.U. Shankar, "A Relational Notation for State Transition Systems," IEEE Transactions on Software Engineering, vol. 16, no. 7, pp. 755-775, July 1990, doi:10.1109/32.56101
Usage of this product signifies your acceptance of the Terms of Use.