Horst F. Wedde und D. C. Daniels
Graph-Theoretical Tools and Their Use in a Practical Operating System Design Case
Graph-theoretic concepts in computer science - international workshop WG ’87 proceedings, Hrsg.: Herbert Gottler und Hans Jurgen Schneider, Nr. 314, Spr, Kloster Banz\slash Staffelstein, Germany, 1988-06-29
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.