Specifying modules to satisfy interfaces: A state transition system approach | Distributed Computing Skip to main content
Springer Nature Link
Log in

Specifying modules to satisfy interfaces: A state transition system approach

  • Published:
Distributed Computing Aims and scope Submit manuscript

Summary

We defineinterface, module and the meaning ofM offers I, whereM denotes a module andI an interface. For a moduleM and disjoint interfacesU andL, the meaning ofM using L offers U is also defined. For a linear hierarchy of modules and interfaces,M 1, I1, M2, I2, ...,M n, In, we present the following composition theorem: IfM 1 offersI 1 and, fori=2, ...,n, M i usingI i−1 offersI i, then the hierarchy of modules offersI n.

Our theory is applied to solve a problem posed by Leslie Lamport at the 1987 Lake Arrowhead Workshop. We first present a formal specification of a serializable database interface. We then provide specifications of two modules, one based upon two-phase locking and the other multi-version timestamps; the two-phase locking module uses an interface offered by a physical database. We prove that each module offers the serializable interface.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abadi M, Lamport L: The existence of refinement mappings. Research Report 29, Digital Systems Research Center, Palo Alto, CA 94301, August 1988

  2. Abadi M, Lamport L: Composing specifications. In: de Bakker, JW, de Roever W-P, Rozenberg G (eds) Stepwise refinement of distributed systems. LNCS vol 430. Springer, Berlin Heidelberg New York 1990

    Google Scholar 

  3. Bernstein PA, Hadzilacos V, Goodman N: Concurrency control and recovery in database systems. Addison-Wesley, Reading, Massachusetts 1987

    Google Scholar 

  4. Chandy KM, Misra J: A foundation of parallel program design. Addison-Wesley, Reading, Massachusetts 1988

    Google Scholar 

  5. Hoare CAR: Communicating sequential processes. Prentice-Hall, Englewood Cliffs, NJ 1985

    Google Scholar 

  6. Jonsson B: On decomposing and refining specifications of distributed systems. In: de Bakker JW, de Roever W-P, Rozenberg G (eds) Stepwise refinement of distributed systems. LNCS vol 430. Springer, Berlin Heidelberg New York 1990

    Google Scholar 

  7. Lam SS, Shankar AU: Protocol verification via projections. IEEE Trans. Software Eng. Vol. SE-10, 10: 325–342 (1984)

    Google Scholar 

  8. Lam SS, Shankar AU: Specifying an implementation to satisfy interface specifications: a state transition approach. 26th Lake Arrowhead Workshop on how will we specify concurrent systems in the year 2000. September 1987

  9. Lam SS, Shankar AU: A relational notation for state transition systems. IEEE Trans. Software Eng 16 (7):755–775 (1990) (an abbreviated version entitled Refinement and Projection of Relational Specifications. In: de Bakker W, de Roever W-P, Rozenberg G (eds) Stepwise refinement of distributed systems) LNCS vol 430. Springer, Berlin Heidelberg New York 1990

    Google Scholar 

  10. Lam SS, Shankar AU: A theory of interfaces and modules, part I and part II. Technical reports, Department of Computer Sciences, University of Texas at Austin, 1992. An abbreviated version of part I entitledUnderstanding Interfaces. In: Proceedings IFIP Fourth International Conference on Formal Description Techniques (FORTE), Sydney, Australia, November 1991

  11. Lamport L: An assertional correctness proof of a distributed algorithm. Sci Comput Program 2: 175–206 (1982)

    Google Scholar 

  12. Lamport L: What it means for a concurrent program to satisfy a specification: why no one has specified priority. Proceedings 12th ACM Symposium on Principles of Programming Languages. New Orleans 1985

  13. Lamport L: A serializable database interface. 26th Lake Arrow-head Workshop on how will we specify concurrent systems in the year 2000. September 1987

  14. Lamport L: A simple approach to specifying concurrent systems. Comm ACM 32 (1):32–45 (1989)

    Google Scholar 

  15. Lynch N, Tuttle M: Hierarchical correctness proofs for distributed algorithms. Proceedings of the ACM Symposium on Principles of Distributed Computing, Vancouver, B.C., August 1987

  16. Lynch N, Merritt M, Weihl W, Fekete A: A theory of atomic transactions. Technical Report MIT/LCS/TM-362, Laboratory for Computer Science, M.I.T, June 1988

  17. Manna Z, Pnueli A: Adequate proof principles for invariance and liveness properties of concurrent programs. Sci Comput Program 4:257–289 (1984)

    Google Scholar 

  18. Misra J, Chandy KM: Proofs of networks of processes. IEEE Trans Software Eng. Vol. SE-7, 4: 417–426 (1981)

    Google Scholar 

  19. Murphy SL, Shankar AU: Service specification and protocol construction for the transport layer, CS-TR-2033, UMIACS-TR-88-38, Computer Science Department University of Maryland, May 1988; an abbreviated version appears in Proc. ACM SIGCOMM '88 Symposium, August 1988

  20. Owicki S, Gries D: An axiomatic proof technique for parallel programs I. Acta Inf 6: 319–340 (1976)

    Google Scholar 

  21. Owicki S, Lamport L: Proving liveness properties of concurrent systems. ACM TOPLAS 4(3):455–495 (1982)

    Google Scholar 

  22. Pnueli A: In transition from global to modular temporal reasoning about programs. NATO ASI Series. In: Logics and models of concurrent systems. Apt KR (ed) vol F13, Springer, Berlin Heidelberg New York 1984. pp 123–144

    Google Scholar 

  23. Shankar AU, Lam SS: An HDLC protocol specification and its verification using image protocols. ACM Trans Comput Syst. Vol. 1, 4: 331–368 (1983)

    Google Scholar 

  24. Shankar AU, Lam SS: A stepwise refinement heuristic for protocol construction. To appear in ACM TOPLAS; an abbreviated version entitled Construction of Network Protocols by Stepwise Refinement. In: de Bakker JW, de Roever W, Rozenberg G (eds): Stepwise refinement of distributed systems. LNCS vol 430. Springer, Berlin Heidelberg New York 1990

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Sciences, The University of Texas at Austin, 78712, Austin, TX, USA

    Simon S. Lam & A. Udaya Shankar

  2. Department of Computer Science and Institute for Advanced Computer Studies, University of Maryland, 20742, College Park, MD, USA

    Simon S. Lam & A. Udaya Shankar

Authors
  1. Simon S. Lam
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. Udaya Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

Simon S. Lam is Chairman of the Department of Computer Sciences at the University of Texas at Austin and holds and endowed professorship. His research interests are in the areas of computer networks, communication protocols, performance models, formal methods, and network security. He serves on the editorial boards ofIEEE Transactions on Software Engineering andPerformance Evaluation. He is an IEEE Fellow, and was a corecipient of the 1975 Leonard G. Abraham Prize Paper Award from the IEEE Communications Society. He organized and was program chairman of the first ACM SIGCOMM Symposium on Communications Architectures and Protocols in 1983. He received the BSEE degree (with Distinction) from Washington State University in 1969, and the MS and Ph.D. degrees from the University of California at Los Angeles in 1970 and 1974 respectively. Prior to joining the University of Texas faculty, he was with the IBM T.J. Watson Research Center from 1974 to 1977.

A. Udaya Shankar received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, Kanpur, in 1976, the M.S. degree in Computer Engineering from Syracuse University, Syracuse, NY, in 1978, and the Ph.D. degree in Electrical Engineering from the University of Texas at Austin, in 1982. Since January 1983, he has been with the University of Maryland, College Park, where he is now an Associate Professor of Computer Science. Since September 1985, he has been with the Institute for Advanced Computer Studies at the University of Maryland. His current research interests include the modeling and analysis of distributed systems and network protocols, from both correctness and performance aspects. He is a member of IEEE and ACM.

The work of Simon S. Lam was supported by National Science Foundation grants no. NCR-8613338 and no. NCR-9004464. The work of A. Udaya Shankar was supported by National Science Foundation grants no. ECS-8502113 and no. NCR-8904590

Rights and permissions

Reprints and permissions

About this article

Cite this article

Lam, S.S., Shankar, A.U. Specifying modules to satisfy interfaces: A state transition system approach. Distrib Comput 6, 39–63 (1992). https://doi.org/10.1007/BF02276640

Download citation

  • Received:

  • Accepted:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02276640

Key words

Search

Navigation