Abstract
We specify and prove correctness of a real-world fault-tolerance algorithm. The algorithm, developed by Chang and Maxemchuk [CM84], guarantees delivery of broadcast messages over a broadcast medium (e.g., an ethernet) in the presence of faults that may cause messages to be lost or only partially delivered. Instead of describing the operation of the algorithm in pseudo-code, as the authors of the algorithm have done, we generate a precise mathematical specification which is amenable to reasonably simple proof techniques. The formal method that we use in this paper is based on modal (state dependent) functions called the modal primitive recursive (m.p.r.) functions. Our analysis clarifies the workings of the algorithm by discarding the complex program scaffolding that obscures the original exposition.
This research was funded in part by the Office of Naval Research under contract N00014-85-K-0398 and N00014-92-J-1048.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J.M. Chang and N.F. Maxemchuk. Reliable broadcast protocols. ACM Trans. Computer Systems, 2(3), august 1984.
Ferenc Gecseg. Products of Automata. Monographs in Theoretical Computer Science. Springer Verlag, 1986.
R. L. Goodstein. Development of Mathematical Logic. Logic Press, London, 1971.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Welsey, Reading MA, 1979.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1979.
E.F. Moore, editor. Sequential Machines: Selected Papers. Addison-Welsey, Reading MA, 1964.
Rozsa Peter. Recursive functions. Academic Press, 1967.
A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of curent trends. In J.W. de Bakker, editor, Current Trends in Concurrency, volume 224 of Lecture Notes in Computer Science. Springer-Verlag, 1985.
K. Voss, H.J. Genrich, and G Rozenberg, editors. Concurrency and Nets: Advances in Petri Nets. Springer-Verlag, 1987.
Victor Yodaiken. A Modal Arithmetic for Reasoning About Multi-Level Systems of Finite State Machines. PhD thesis, University of Massachusetts (Amherst), 1990.
Victor Yodaiken. The algebraic feedback product of automata. In Papers from the DIMACS Workshop on Computer Aided Verification, AMS-DIMACS Series. American Mathematical Society, 1991.
Victor Yodaiken. Modal functions for concise representation of finite automata. Information Processing Letters, to appear 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yodaiken, V., Ramamritham, K. (1991). Verification of a reliable net protocol. In: Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1992. Lecture Notes in Computer Science, vol 571. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55092-5_11
Download citation
DOI: https://doi.org/10.1007/3-540-55092-5_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55092-1
Online ISBN: 978-3-540-46692-5
eBook Packages: Springer Book Archive