An Algebraic-Temporal Specification of a CSMA/CD-Protocol
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.
KeywordsCommunication protocols formal methods stepwise development refinements algebraic specifications and temporal logic.
- Abrial, J. R. (1985), Programming as a mathematical exercise, in C. Hoare, ed., ‘Mathematical Logic and Programming Languages’, Prentice-Hall International.Google Scholar
- 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
- 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
- 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
- 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
- Inf (1987), LOTOS - A formal description technique based on temporal ordering of observational behaviour. (ISO/TC 97/SC 21N).Google Scholar
- 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
- 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
- Milner, R. (1980), A Calculus for Communication Systems, Vol. 90 of Lecture Notes in Computer Science, Springer, Berlin.Google Scholar
- 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
- 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