Advertisement

An Algebraic-Temporal Specification of a CSMA/CD-Protocol

  • Mohamed Jmaiel
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

This paper presents a formal development of a CSMA/CD (Carrier Sense, Multiple Access with Collision Detection) protocol. Using a combination of temporal logic and algebraic specifications we describe the message layout and the behavioral aspects of the protocol in a unified framework. We benefit from the deduction system of temporal logic to establish safety and liveness properties of the protocol.

Keywords

Communication protocols formal methods stepwise development refinements algebraic specifications and temporal logic. 

References

  1. Abrial, J. R. (1985), Programming as a mathematical exercise, in C. Hoare, ed., ‘Mathematical Logic and Programming Languages’, Prentice-Hall International.Google Scholar
  2. Ame (1985), Local Area Networks: Carrier Sense Multiple Access with Collision Detection (CSMA/CD) Access Method and Physical Layer Specifications. ANSI/IEEE Standard 802.3.Google Scholar
  3. Barringer, H., Kuiper, R. & Pnueli, A. (1984), Now you may compose temporal specifications, in ‘Proceeding of the 16th ACM Symposium on Theory of Computing’, pp. 51–63.Google Scholar
  4. Bjørner, D. & Jones, C. B. (1987), The vienne development method: the meta-language, Vol. 280 of Lecture Notes in Computer Science, Springer Verlag, Berlin.Google Scholar
  5. Broy, M. (1988), Requirement and design specification for distributed systems, in F. Vogt, ed., ‘Concurrency’, Vol. 335 of Lecture Notes in Computer Science, Springer, Berlin, pp. 33–62.Google Scholar
  6. Ehrig, H. & Mahr, B. (1985), Fundamentals of Algebraic Specification 1, EATCS Monographs on Theoretical Computer Science, Springer, Berlin.CrossRefzbMATHGoogle Scholar
  7. Hoare, C. (1985), Communicating Sequential Processes Prentice Hall International.zbMATHGoogle Scholar
  8. Inf (1987), LOTOS - A formal description technique based on temporal ordering of observational behaviour. (ISO/TC 97/SC 21N).Google Scholar
  9. Jmaiel, M. & Pepper, P. (1994), Development of communication protocols using algebraic and temporal specifications, in ‘Proceedings of the International Workshop on Advanced Software Technology, Shanghai, Sept. 15–16 1994.’, Jiao Tong University, Shanghai.Google Scholar
  10. Koymans, R. (1992), Specifying Message Passing and Time-Critical Systems with Temporal Logic, Vol. 651 of Lecture Notes in Computer Science, Springer, Berlin.CrossRefGoogle Scholar
  11. Lichtenstein, O., Pnueli, A. & Zuck, L. (1985), The glory of the past, in ‘Proc. of the Workshop on Logics of Programs 85’, Vol. 193 of Lecture Notes in Computer Science, Springer, Berlin, pp. 196–218.Google Scholar
  12. Milner, R. (1980), A Calculus for Communication Systems, Vol. 90 of Lecture Notes in Computer Science, Springer, Berlin.Google Scholar
  13. Pepper, P. & Wirsing, M. (1994), KORSO: a Methodology for the Development of Correct Software, in M. Broy & S. Jähnichen, eds, ‘KORSO, Correct Software by Formal Methods’, Lecture Notes in Computer Science, Springer.Google Scholar
  14. Petri, C. A. (1962), Fundamantals of a theory of asynchronous information flow, in Proc. of the IFIP Congress 1962, Munich’, North Holland Publishing Company, Amsterdam, pp. 386–390.Google Scholar
  15. Sistla, A., Clarke, E., Francez, N. & Meyer, A. (1984), ‘Can message buffers be axiomatized in linear temporal logic?’, Information and Control 63, 88–112.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • Mohamed Jmaiel
    • 1
  1. 1.Technische Universität BerlinBerlinGermany

Personalised recommendations