REGIS-DARWIN specified in the π-calculus

Summary form only given. REGIS is a programming system for the development of distributed and parallel programs. REGIS programs consist of three parts. Firstly, there is a configuration part, written in the DARWIN language, which provides a hierarchical structure of components with dynamic binding. Secondly, there is the actual communication part which provides the interaction and synchronisation required by the system. Finally, there is the computation part providing the component programs written in C++. The subdivision of concurrent programs into the three separate parts of organisation, communication and computation leads to programs that are easy to specify, compile and execute. An important characteristic of the REGIS-DARWIN system is that it enables systems to be configured dynamically by making the addresses of ports first class objects. In order to specify precisely the behaviour of REGIS-DARWIN programs, we have translated the organisation and communication primitives into the π-calculus, a formalism for modelling concurrent processes. The π-calculus semantics enables us to deduce behavioural properties of REGIS-DARWIN programs