Towards Dynamic Population Management of Abstract Machines in the B Method

We study some restrictions associated with the mechanisms for structuring and modularising specifications in the B abstract machine notation. We propose an extension of the language that allows one to specify machines whose constituent modules (other abstract machines) may change dynamically, i.e., at run time. In this way, we increase the expressiveness of B by adding support for a common activity of the current systems design practice.The …