Abstract
Practical problems in developing large distributed systems (stemming e.g. from the real size of the system) regularly encounter several severe constraints that are not to be found in theoretical discussions when dealing with the abstract mirror image of the original problems. In this paper we report on part of our practical experience with the Theory of Interaction Systems which we used for designing the resource management of the completely distributed operating system DRAGON SLAYER, and even for verifying the actual implemented code. This had evolved into two different formal modeling problems since the distributed code which resulted from our first attempt (top-down approach) was changed and streamlined, for improving its efficiency, to such an extent that a completely new formal model had to be constructed in oder to prove the correct functioning of DRAGON SLAYER's resource scheduling algorithm. After introducing into the Theory of Interaction Systems as well as into the first formal model for the top-down design, we describe the incremental procedure of building a formal model for the implemented distributed algorithm. Hints for the correctness proof are given. The practicality of our theoretical approach is stressed throughout and finally discussed in detail.
This work was partially supported by IBM Endicott (Research Agreement No. 6073-86) and by the State of Michigan (IPPRI-85-140625 and IMR-86-146751).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
G.V. BOCHMANN, Finite-State Description of Communication Protocols; Computer Networks Vol. 2(1978)
B. BOSCHMANN, Zur Verhaltensanalyse in verteilten Systemen. Diploma Thesis, Bonn 1984 (German)
H.-D. BREMER, Planung in Grossunternehmen mit Hilfe der Interaktionssysteme. Diploma Thesis, Bonn 1984 (German)
G. CASTELLI, F. DE CINDIO, G. DE MICHELIS, C. SIMONE, The GCP Language and its Implementation; Proc. of the IFIP workshop "Languages for Automation"; New Orleans, October 1984
M. CHANDY, J. MISRA, An Example of Stepwise Refinement of Distributed Programs: Quiescence Detection; TOPLAS Vol. 8 No. 3(1986)
M. CHANDY, J. MISRA, The Drinking Philosophers' Problem; TOPLAS Vol. 6 No.4 (1984)
F. DE CINDIO, G. DE MICHELIS, L. POMELLO, C. SIMONE, A Petri Net Model of CSP; Proc. of the CIL'81, Barcelona 1981
D.C. DANIELS; DRAGON SLAYER: A Blueprint for the Design of a Completely Distributed Operating System; Master's Thesis, Wayne State University 1986
D.C. DANIELS, H.F. WEDDE, Real-time Performance of a Completely Distributed Operating System; Proc. of the IEEE Real-time Systems Symp.'86, New Orleans, December 1986
C.B. FRIEDLANDER, H.F. WEDDE, Distributed Processing under the DRAGON SLARYER Operating System; Proc. of the 15th International IEEE Conference on Parallel Processing, Pheasant Run Resort, August 1986
C.A.R. HOARE, Communicating Sequential Processes; CACM Vol. 21 No. 8(1978)
A. MAGGIOLO-SCHETTINI. H.F. WEDDE, J. WINKOWSKI, Modeling a Solution for a Control Problem in Distributed Systems by Restrictions; Theoretical Computer Science 13 (1981)
A. PNUELI, The Temporal Semantics of Concurrent Programming; in G. Kahn, R. Milner (ed.): Springer Lecture Notes in Computer Science Vol. 70(1979)
A.S. TANENBAUM, R. VAN RENESSE, Distributed Operating Systems; ACM Computing Surveys Vol. 17 No. 4(1985)
H.F. WEDDE, A Graph-theoretic Model for Designing Fair Distributed Scheduling Algorithms; in Tinhofer, Schmidt (ed.): Springer Lecture Notes in Computer Science Vol. 246(1987)
H.F. WEDDE, A Formal Basis for Correct Implementation of Distributed Programming Languages; Proc. of the 5th International IEEE Conference on Distributed Computing Systems, Denver, May 1985
H.F. WEDDE, Value of Formal Information System Models for a Flexible Reorganization in an Insurance Company; in J.C. Agrawal, P. Zunde (ed.): Empirical Foundations of Software and Systems Sciences; Plenum Press 1985
H.F. WEDDE, An Iterative and Starvation-free Solution for a General Class of Distributed Control Problems Based on Interaction Primitives; Theoretical Computer Science Vol. 24 (1983)
J. WINKOWSKI, Protocols of Accessing Overlapping Sets of Resources; Information Processing Letters Vol. 12 No. 5(1981)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wedde, H.F., Daniels, D.C. (1988). Graph-theoretical tools and their use in a practical distributed operating system design case. In: Göttler, H., Schneider, HJ. (eds) Graph-Theoretic Concepts in Computer Science. WG 1987. Lecture Notes in Computer Science, vol 314. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19422-3_15
Download citation
DOI: https://doi.org/10.1007/3-540-19422-3_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19422-4
Online ISBN: 978-3-540-39264-4
eBook Packages: Springer Book Archive