Skip to main content
SpringerLink
Log in

From state machines to temporal logic: Specification methods for protocol standards

  • 2. Tutorial Papers
  • Conference paper
  • First Online:
The Analysis of Concurrent Systems

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 207))

Abstract

This paper attempts to lend perspective to several different methods that have been employed for specifying computer communication protocols by comparing a spectrum of specification techniques. The paper characterizes specification languages such as state transition diagrams, variants of temporal logic approaches, and sequence expressions by the extent to which information is encoded as properties of a single state versus properties of a history of the entire computation state sequence. Taking the prototypical alternating bit protocol as an example, each method is used to specify the requirements for the send process of the distributed system.

This work was supported by the National Science Foundation under Grant MCS-8104459 and by the Defense Communications Agency under Contract DCA 100-80-C-0044.

The authors are with the Computer Science Laboratory, SRI International, Menlo Park, CA 94025.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ISO TC97/SC 16/WG1 Subgroup A on Architecture, “Concepts for describing the OSI architecture.” working draft, Ispra, Nov. 1981.

    Google Scholar 

  2. D. Lehmann, A. Pnueli, and J. Stavi, “Impartiality, justice and fairness: The ethics of concurrent termination,” in Proc. ICALP 81. New York: Springer Verlag, July 1981.

    Google Scholar 

  3. Z. Manna and A. Pnueli, “Verification of concurrent programs, Part I: The temporal framework,” Dep. Comput. Sci., Stanford Univ., Stanford, CA, Tech. Rep. STAN-CS-81-836, June 1981.

    Google Scholar 

  4. B. Hailpem, “Verifying concurrent processes using temporal logic,” Comput. Syst. Lab., Stanford Univ., Stanford, CA, Tech. Rep. 195, Aug. 1980.

    Google Scholar 

  5. ISO TC97/SC16/WG1 Subgroup B on State Machines, “A FDT based on an extended state transition model,” working draft, Boston, MA, Dec. 1981.

    Google Scholar 

  6. O. Herzog, “Static analysis of concurrent processes for dynamic properties using Petri nets,” in Semantics of Concurrent Computation. Evian, France: Springer Verlag, 1979.

    Google Scholar 

  7. L. Lamport, “Specifying concurrent program modules,” Comput. Sci. Lab., SRI Int., June 1981; also TOPLAS, to be published.

    Google Scholar 

  8. F. Vogt, “Event-based temporal logic specification of distributed systems,” Ph.D. dissertation, Hahn-Meitner Inst., Berlin, Germany, Feb. 1982.

    Google Scholar 

  9. P. Wolper, “Specification and synthesis of communicating processes using an extended temporal logic,” in Proc. POPL 82, ACM, Albuquerque, NM, Jan. 1982.

    Google Scholar 

  10. S. Schindler, “Basic concepts of formal specification techniques and of RSPL,” Tech. Univ. Berlin, Berlin, Germany, Tech. Rep., May 1980.

    Google Scholar 

  11. ISO/TC97/SC16/WG1 Subgroup on Temporal Ordering Expressions, “Interaction primitives in formal specification of distributed systems,” working paper, Washington, DC, Sept. 1981.

    Google Scholar 

  12. P. E. Lauer, P. Torrigiani, and M. Shields, “COSY: A system specification language based on paths and processes,” Acta Inform., vol. 12, pp. 109–158, 1979.

    Google Scholar 

  13. R. L. Schwartz and P. M. Melliar-Smith, “Temporal logic specification of distributed systems,” in Proc. IEEE Conf. Distributed Syst., Apr. 1981 (revised version available from the authors).

    Google Scholar 

  14. L. Lamport, “Sometime is sometimes not never,” in Proc. POPL 1980, ACM, Las Vegas, NV, Jan. 1980.

    Google Scholar 

  15. B. Berthomieu, “Algebraic specification of communication protocols,” Inform. Sci. Inst., Univ. Southern California. Los Angeles. Tech. Rep. RR-81-98, Dec. 1981.

    Google Scholar 

  16. S. Gerhart et al., “An overview of AFFIRM: A specification and verification system,” in Proc. IFIP Congress 80, Oct. 1980.

    Google Scholar 

  17. R. E. Shostak, R. L. Schwartz, and P. M. Melliar-Smith, “STP: A mechanized logic for specification and verification,” in Proc. 6th Conf. Automated Deduction (Lecture Notes in Computer Science, vol. 138). New York: Springer Verlag, June 1982.

    Google Scholar 

Download references

Authors
  1. Richard L. Schwartz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. Michael Melliar-Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

B. T. Denvir W. T. Harwood M. I. Jackson M. J. Wray

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schwartz, R.L., Melliar-Smith, P.M. (1985). From state machines to temporal logic: Specification methods for protocol standards. In: Denvir, B.T., Harwood, W.T., Jackson, M.I., Wray, M.J. (eds) The Analysis of Concurrent Systems. Lecture Notes in Computer Science, vol 207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16047-7_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-16047-7_35

  • Received:

  • Revised:

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16047-2

  • Online ISBN: 978-3-540-39731-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation