A dynamic extension for the specifications of distributed systems

Describes an approach for extending distributed system specifications. These specifications are structured as a parallel composition of subsystem specifications. The approach consists of building a new specification S_new by adding a new behavior described by a specification S_added to a specification S_old with preservation of the properties of S_old and S_added as well as the structure of S_old. S_new has all the properties of S_old and S_added if S_new can perform whatever S_old (and S_added) can perform and if it does not block where S_old (or S_added) does not block. We apply our approach to extending the functionality of a basic automatic teller machine