Formal specification and analysis for reliable and transparent resource management

A report is presented on the design and implementation of a novel, highly reliable resource management algorithm which functions within the distributed operating system DRAGON SLAYER. The particular design goals for DRAGON SLAYER include not only reliability of services in face node or link failures, or in face of unreliability on the software level, but also a novel form of resource transparency in the absence of any global control or information. It is necessary to deal with a very difficult and general conceptual problem calling for a solution that further had to satisfy requirements of practicality. The design of the algorithm is based on a formal model, the theory of interaction systems. The authors prove the correctness (fairness) of the algorithm in the formal model. The construction method for this model is modular and incremental.<>