A model of reconfiguration in communicating sequential processes with a notion of transactions (Q1186564)

The author gives a model of reconfigurable systems in Hoare's Communicating Sequential Processes (CSP). The purpose of such a model is to facilitate reasoning about reconfigurable systems. Jacob's model has been used by \textit{Edwards} to reason about reconfigurable systems. An important characteristic of the model is the separation of the structure of the system, which may be reconfigured, from the configurations into which it may be put. Unfortunately there is a problem with this model. It allows a system to be reconfigured at any moment in its life. This is often too liberal: usually systems may be reconfigured only between transactions. Ad hoc solutions to this problem are possible, and this is the solution \textit{Edwards} uses. Our solution takes account of the transactions a system can perform, while maintaining as much as possible of the orthogonality between the system structure and the configurations in which it can occur.