Formalizing System Structure

摘要

Darwin is a language designed for configuring distributed systems. A system is modelled as a decompositional hierarchy of components with interfaces. Connections are represented as bindings between interfaces. Darwin programs define component types. Configurations of a system are obtained by instantiating these types. Configurations have to comply with a number of constraints on the system structure. It is therefore intuitive to express these constraints in the domain of configurations rather than on the language level. To succeed in this endeavour we need to precisely express the relation between Darwin programs and configurations. We do this in terms of a first-order logic theory of Darwin programs and configurations. Models of the theory provide a straightforward mapping from Darwin programs to configurations and vice versa. Most of the constraints on configurations as well as structural transformations can be specified by adding just a few axioms to the theory. Also the theory enables us to generate Darwin programs from configurations thus allowing for the inclusion of existing systems into new programs.